SMV model-based safety analysis of software requirements

Abstract

Software control in safety-critical systems such as aerospace, military, nuclear power plant, and medical applications has become increasingly common in recent years. When software is used as a control agent in these systems, safety becomes a paramount concern. In the worst case, software malfunctions, i.e. unsafe software control outputs can result in serious and unacceptable consequences such as death, injury, or environmental damage Of all the phase in software development, the requirements analysis phase is generally considered to play the most critical role in determining the overall software safety and quality because defective requirements specifications may result in errors which propagate to subsequent phases of software development and mistakes made during the requirements analysis phase can easily introduce faults which subsequently lead to accidents. Fault tree analysis is one of the most frequently applied safety analysis techniques when developing safety-critical industrial systems such as software-based emergency shutdown systems of nuclear power plant, and it has been used for safety analysis of software requirements in nuclear industry. However, conventional method for safety analysis of software requirements has problems. The problems are that fault tree generated from natural language specification may contain flaws and manual safety verification work is labor-intensive and time-consuming. When synthesizing fault tree from natural language, errors can be made because of informality of natural language as well as that of the fault tree. However, this problem can be resolved by using formal model, instead of natural language, i.e. formal factor of the formal model can be helpful to reduce errors of fault tree. Since automatic verification from formal model is possible, the problem of manual safety verification can be also resolved. In this study, we propose a new approach to resolve problems of conventional method for safety analysis of softwar...