Systems Engineering and Electronics ›› 2018, Vol. 40 ›› Issue (7): 1654-1659.doi: 10.3969/j.issn.1001-506X.2018.07.34

Previous Articles     Next Articles

Model-checking oriented unified modeling method based on NuSMV

CHEN Lu, JIAO Jian, WEI Qianxin   

  1. School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China
  • Online:2018-06-26 Published:2018-06-28

Abstract:

Formal modeling and automated analysis and verification based on model checking are the core of the model based safety analysis (MBSA) technology. MBSA has gained wide attention and application in the safety work of large complex equipment system, for the reason that it improves the work efficiency and objectivity of the analysis results. The existing modeling process under the MBSA framework is relatively complex, and often needs model transformation, which results in information loss easily and affects the accuracy and completeness of safety analysis results. A model-checking oriented unified system modeling method using symbolic language is proposed, including the mapping relationships between the formal language elements and system functions, architecture and fault modes as well as the normalized definitions of system safety requirements using temporal logic formulas. Finally, a case study about the actuator system of the flight control system is provided to validate the availability and applicability of the modeling method.

[an error occurred while processing this directive]