一句话：提出FREPA方法、领域语言AASRDL及工具AeroReq，支持航空控制需求形式化建模与V&V并落地工业。
形式化方法有望用于系统需求建模与分析，但在大型工业项目中落地仍困难：工程师缺乏自动化工程方法构建精确需求模型并严格验证与确认。为此，作者提出系统化工程方法FREPA，其为学术界与工业界八年合作成果。FREPA提供自动化需求建模与V&V流程，配套领域特定建模语言AASRDL描述形式化规约，以及实用工具AeroReq。作者在7个真实航天手势控制系统和2个航空发动机控制系统上应用FREPA。结果表明，FREPA与AeroReq显著促进了工业形式化建模与V&V，并总结了经验教训。
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.
DOI 原文 ·
@inproceedings{paperbot5854,
title = {FREPA: an automated and formal approach to requirement modeling and analysis in aircraft control domain},
author = {Jincao Feng and Weikai Miao and Hanyue Zheng and Yihao Huang and Jianwen Li and Zheng Wang and Ting Su and Bin Gu and Geguang Pu and Mengfei Yang and Jifeng He},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3417047}
}