FREPA:一种面向飞机控制领域需求建模与分析的自动化形式化方法
软件工程
2023-06-05 v1
摘要
形式化方法在系统需求建模与分析方面颇具前景。然而,将形式化方法应用于大规模工业项目仍是一项挑战。工业工程师苦于缺乏自动化工程方法论,以有效构建精确的需求模型,并对所生成的模型进行严格的验证与确认(V&V)。为应对这一挑战,本文提出一种系统化工程方法,称为飞机形式化需求工程平台(FREPA),用于航空航天与航空控制领域的形式化需求建模与V&V。FREPA是学术界与工业界过去八年无缝协作的成果。本文的主要贡献包括:1)一种自动化、系统化的工程方法FREPA,用于在航空航天与航空控制领域构建需求模型、验证与确认系统;2)一种用于描述形式化规约的领域专用建模语言AASRDL;3)一个实用的基于FREPA的工具AeroReq,该工具已被我们的工业合作伙伴使用。我们已成功将FREPA应用于七个真实的航空航天手势控制系统和两个航空发动机控制系统。实验结果表明,FREPA及相应工具AeroReq显著促进了工业中的形式化建模与V&V。此外,我们还讨论了在航空航天与航空项目中应用FREPA所获得的经验与教训。
引用
@article{arxiv.2306.01260,
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},
journal= {arXiv preprint arXiv:2306.01260},
year = {2023}
}
备注
12 pages, Published by FSE 2020