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

Computer Engineering & Science

Previous Articles     Next Articles

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

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