A model-checking oriented modeling method for safety critical system

In the development of safety-critical system, ModelBased Safety Assessment (MBSA) process can reduce the development complexity and improve assessment efficiency. As an important part of MBSA, system modeling and safety requirements description with formal methods still lack a well-defined process. In this paper, the relationship between traditional safety assessment process and MBSA is discussed, a system modeling and safety property formalization method based on NuSMV is proposed. Finally, a case study is presented to demonstrate and validate the proposed modeling method.