• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 软件工程 • 上一篇    下一篇

航空机载嵌入式控制软件需求建模的形式化工程方法

黄怿豪,冯劲草,郑寒月,缪炜恺,蒲戈光   

  1. (华东师范大学上海市高可信重点实验室,上海 200062)
  • 收稿日期:2018-11-15 修回日期:2019-01-05 出版日期:2019-06-25 发布日期:2019-06-25
  • 基金资助:

    国防科工局项目(JCKY 2016212B0042)

A formal engineering method for requirement
modeling of airborne embedded control software

HUANG Yihao,FENG Jincao,ZHENG Hanyue,MIAO Weikai,PU Geguang   

  1. (Shanghai Key Laboratory of Trustworthy Computing,East China Normal University,Shanghai 200062,China)
  • Received:2018-11-15 Revised:2019-01-05 Online:2019-06-25 Published:2019-06-25

摘要:

嵌入式控制软件是现代航空飞行器的核心部件之一。构建软件需求的形式化规约精确地刻画人们对软件期望的功能和运行场景,是确保此类安全攸关软件质量的根本途径。在工业界,形式化需求建模的大规模应用尽管有成功的案例,但仍面临众多的困难。其根本性难点在于缺少一种系统化的工程方法来引导工业界软件实践者,从原始需求开始最终完成形式化需求规约,并能确认该规约真实、充分地反映了人们对软件期望的功能。针对上述挑战,提出了一种面向机载控制软件需求建模的形式化工程方法ACSDLMV,以形式化方法为理论基础,结合软件需求工程的基本原理,引导工程人员从原始需求出发以演化式的过程逐步完成需求规约的构建;定制了航空控制软件的形式化描述语言ACSDL,用以构建形式化规约;为了确认软件需求规约准确、充分地描述了人们对软件期望的功能,该方法给出了基于图形的静态审查和基于模型的动态模拟技术。在航空发动机公司中的实验结果表明,该方法相比传统方法探测到了更多的潜在错误。
 
 

关键词: 软件需求建模, 需求确认, 形式化工程方法, 形式化方法

Abstract:

Embedded control software is one of the core components of modern aerocrafts. Constructing formal requirement specification to accurately describe the intended functions and operational scenarios is recognized as a fundamental way to ensure the quality of such safety-critical software. However, industrial practitioners still face a big challenge of applying formal modeling in largescale software projects due to the lack of a systematic engineering approach. Such an approach should provide practical technologies for guiding practitioners to construct formal specifications from the scratch and validate whether the specifications conform to the intended functions and scenarios. To tackle this challenge, we propose a formal engineering method called aero control software description language based modeling and validation (ACSDL-MV) for the requirement modeling of airborne control software. The ACSDL-MV incorporates formal methods and traditional software engineering technologies by guiding practitioners to build formal specifications from the original requirement document in an evolutionary process. For building formal specifications, we design a formal description language of airborne control software, which is named aero control software description language (ACSDL). In order to confirm that the requirement specifications accurately and sufficiently describe software capabilities expected by people, we provide static review based on diagram and dynamic simulation based on formal model. Experimental results show that the approach can detect more potential errors than traditional review methods.

 

 

Key words: software requirements modeling, requirement validation, formal engineering method, formal method