随着大量软件在工业界的广泛应用,越来越多的嵌入式系统的核心控制软件逐渐走向数字化控制的道路。随着计算机硬件性能的逐渐提升,人们期待用计算机去解决的问题越来越困难,这也导致现代工业控制软件日益庞大与复杂。在这种情况下,如何在安全攸关系统中保障系统的安全性显得愈加重要。工业界和学术界都认为对软件开发的起始点对系统需求进行形式化分析与验证是保障嵌入式系统软件可靠性的一个重要手段,然而,如何在工业界的大型软件项目中应用形式化方法仍然是一个亟待解决的难题。工程师在生产实践中应用形式化方法时,仍缺少自动化的工程性方法来高效地选择和建立更加精准的需求模型与性质,且缺少严谨的方法论去确认和验证所建立的需求模型。为了解决上述问题,本文针对形式化方法在工业界中的应用进行了研究和探索,其主要的研究内容和贡献如下:·设计了一个领域专用的轻量级需求建模语言AASRDL在特定嵌入式领域中,通用的建模语言学习曲线陡峭,学习成本巨大,无法满足工程师快速建模的需求,为了解决这一难题,通过总结相应的嵌入式领域特征,本文设计了一个轻量级领域专用的需求建模语言AASRDL,用于需求规约的快速构建。同时,本文还提供了一个模板来引导构建形式化需求模型;·提出了一种基于NLP的需求规约自动生成方法为了解决工程师难以熟练使用形式化语言描述待验证的安全性质问题,提出了一个可以将自然语言描述的性质转化为需求规约的方法。通过分析安全需求的性质描述特征,提出了一个安全需求的语义模型,使用句法切块技术和依存关系分析技术进行安全需求中的信息抽取并将其存储在语义模型中,并最终根据目标语言翻译成相对应的需求规约;·提出了一个系统性工程方法FREPA提出了一个系统性的可以指导工业界在嵌入式领域中进行形式化需求建模和确认验证的方法FREPA;该系统性的方法主要包括在嵌入式系统中如航空航天系统进行系统需求模型的构建、确认和验证操作,主要分析技术包括基于图标的需求审查、模型模拟执行、基于MC/DC覆盖准则的测试用例自动生成、性质验证;·支撑工具及其应用本文开发了基于FREPA方法的支撑工具,该工具可以实现需求建模和确认验证的自动化操作,并在相应的实际项目中进行了实验和验证。目前为止,本文所提出的方法已经成功地被应用于七个航天飞行器和两个航空发动机控制系统的软件开发过程中。实验表明本文的方法论及其支撑工具工具能够在实际项目中进行有效的形式化建模和确认验证。