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 software requirements. Our approach is that fault tree is generated from SMV (Symbolic Model Verifier) model and safety properties are verified by model checker, SMV. The SMV system is used for our approach because it supports both input language for system modeling and model checking tool for verifying system properties.
To synthesize fault tree from SMV model, synthesis procedure is suggested, and two forms of formulas are proposed for verification of safety properties. One is for checking the existence of node event, and the other one is for checking the correctness of causal relationship among nodes.
To demonstrate the feasibility of our approach, the proposed analysis method is applied into shutdown system 2 (SDS2) of Wolsong nuclear power plant (NPP). In case study, we compare a fault tree from natural language with a fault tree from SMV model considering two points; whether a fault tree from SMV model can cover all contents (or information) of a fault tree from natural language and whether our approach is helpful for reducing errors which can occur in the middle of the synthesis of a fault tree from natural language.
Finally, automatic verification of safety properties obtained by fault tree analysis (FTA) and analysis of the verification result is done. Based on the analysis, we can conclude that a software system is free from a particular hazard or a particular hazard is indeed possible.
항공우주산업, 국방산업, 원자력 발전소 및 의료산업에서 사용되는 응용 프로그램과 같이 소프트웨어로 제어되는 안전이 중요한 시스템들은 최근 들어 매우 보편화 되었다. 소프트웨어를 이러한 시스템을 제어하는데 사용할 때, 소프트웨어의 안전성 문제는 매우 중요하다. 왜냐하면, 최악의 경우 소프트웨어의 오작동이 인간의 생명을 위협할 수 있는 매우 심각한 결과를 초래할 수 있기 때문이다.
소프트웨어를 개발하는 모든 단계 중, 요구사항 분석 단계는 소프트웨어의 전반적인 안전성과 질을 결정하는데 있어 가장 중요한 단계로 여겨지고 있다. 왜냐하면 불완전한 요구사항이 소프트웨어 개발을 위한 그 이후의 단계로 전해져 소프트에어의 오류를 야기시킬 수 있고, 요구사항 분석 단계에서 범해진 실수들은 쉽게 사고로 이어질 수 있기 때문이다.
고장수목 분석기법은 원자력 발전소의 긴급 정지 시스템과 같은 안전성이 중요한 산업 시스템을 개발할 때 가장 많이 사용되는 안전성 분석기법 중에 하나이며, 원자력 산업에서도 소프트웨어 요구사항에 대한 안전성 분석을 위해 사용되어왔다. 그러나 고장수목을 이용한 기존의 방법은 문제점들이 존재하는데, 자연어 명세로부터 생성된 고장수목이 결함을 가질 수 있다는 점과 고장수목 분석기법에서 얻어진 시스템의 안전속성을 사람의 손으로 일일이 검증해야 하는 작업이 노력과 시간이 매우 많이 든다는 점이다.
자연어로부터 고장 수목을 생성 할 때 고장수목 분석기법의 비정형성뿐만 아니라 자연어가 가지는 고유의 비정형성 때문에 오류가 발생할 수 있다. 그러나 이러한 문제는 정형어의 정형성이 이러한 오류를 감소시키는데 도움이 될 수 있으므로, 자연어로부터가 아닌 정형모델로부터 고장수목을 생성하면 해결될 수 있다. 또한 정형모델은 시스템 특성들의 자동 검증이 가능하기 때문에 노력과 시간을 크게 절약할 수 있다.
본 연구에서는, 기존의 요구사항 안전성 분석 방법의 문제점을 해결할 수 있는 새로운 방법을 제안하였는데,. 그 방법은 SMV 모델로부터 고장수목을 생성하고 다시 SMV를 사용해서 시스템의 안전관련 속성들을 검증하는 일련의 과정이다. SMV 시스템은 시스템을 모델링 할 수 있는 입력언어와 시스템 속성을 검증할 수 잇는 모델체커로서의 기능을 모두 제공하기 때문에 본 연구에서 사용되었다.
또한 SMV 모델로부터 고장수목을 생성하기 위해 생성절차와 안전속성 검증을 위해 두 가지 형태,. 즉 노드 사건의 존재성을 검증하는 공식과 노드간의 인과관계의 정확성을 검증하는 공식을 제안하였다.
제안한 방법의 실용 가능성을 증명하기 위해 월성 원자력 발전소의 SDS 2 시스템에 적용해 보았다. 사례 연구에서 SMV 모델을 바탕으로 만들어진 고장수목이 자연어를 바탕으로 만들어진 고장수목의 모든 내용과 정보들을 모두 표현할 수 있는가와, 자연어로부터 고장수목을 생성할 때 발생할 수 있는 오류를 줄일 수 있는가를 알아보기 위해 두 고장수목을 비교하였다.
마지막으로 고장수목 분석을 통해 얻어진 시스템 안전속성을 자동검증하고 그 결과를 분석하였다. 분석결과를 통해 소프트웨어 시스템이 특정한 위험으로부터 안전한지 혹은 그렇지 않은 지를 확인할 수 있었다.