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.

I. Introduction

The traditional safety assessment process based on MIL-STD-882E [1], ARP 4754A/4761 [2], [3] has been widely used in aviation, aerospace, automotive and medical industries. In last two decades, the development of computer science and IC manufacture process promoted the deep integration of mechanical and electrical systems, and sharp increased system complexity. Moreover, the embedded software control style gradually replaced the traditional mechanical control, which makes the system indigestion. Traditinal safety assessment methods which rely heavily on experience have some problems such as the weakness of describe ability, inaccurate result and poor iteration.