Formal methods are promising for modeling and analyzing system requirements. However, applying formal methods to large-scale industrial projects is a remaining challenge. The industrial engineers are suffering from the lack of automated engineering methodologies to effectively conduct precise requirement models, and rigorously validate and verify (V&V) the generated models. To tackle this challenge, in this paper, we present a systematic engineering approach, named Formal Requirement Engineering Platform in Aircraft (FREPA), for formal requirement modeling and V\&V in the aerospace and aviation control domains. FREPA is an outcome of the seamless collaboration between the academy and industry over the last eight years. The main contributions of this paper include 1) an automated and systematic engineering approach FREPA to construct requirement models, validate and verify systems in the aerospace and aviation control domain, 2) a domain-specific modeling language AASRDL to describe the formal specification, and 3) a practical FREPA-based tool AeroReq which has been used by our industry partners. We have successfully adopted FREPA to seven real aerospace gesture control and two aviation engine control systems. The experimental results show that FREPA and the corresponding tool AeroReq significantly facilitate formal modeling and V&V in the industry. Moreover, we also discuss the experiences and lessons gained from using FREPA in aerospace and aviation projects.

翻译：形式化方法在系统需求建模与分析方面具有良好前景。然而，将形式化方法应用于大规模工业项目仍是一项持续挑战。工业工程师因缺乏自动化工程方法论，无法有效构建精确需求模型，并对所生成模型进行严格验证与确认（V&V）。为应对这一挑战，本文提出一套名为"航空领域形式化需求工程平台"（FREPA）的系统化工程方法，用于航空航天与航空控制领域的形式化需求建模及V&V。FREPA是学术界与工业界历时八年密切合作的成果。本文主要贡献包括：1）提出自动化、系统化的工程方法FREPA，用于构建航空航天与航空控制领域的需求模型并验证系统；2）设计领域特定建模语言AASRDL以描述形式化规约；3）开发基于FREPA的实用工具AeroReq，已被工业合作方采用。我们成功将FREPA应用于七个真实航天姿态控制系统与两个航空发动机控制系统。实验结果表明，FREPA及配套工具AeroReq显著促进了工业领域的形式化建模与V&V工作。此外，本文还讨论了在航空航天项目中应用FREPA的经验与教训。