Computer controlled safety-critical systems are increasingly becoming a routine and integral part of modern society. Examples include fly-by-wire aircraft and emergency shutdown systems for nuclear power plants. Safety assurance requirements for such systems are very demanding (e.g., requiring failure probabilities as low as $10^{-9}$) with national and international regulation bodies routinely requiring rigorous safety demonstrations.
Of all the phases in software development, requirements engineering is generally considered to play the most critical role in determining the overall software quality. NASA data \cite{Lut96} demonstrate that nearly $75\%$ of failures found in operational software were caused by errors in the requirements.
Various approaches have been suggested for developing high-quality SRS and conducted cost-effective analysis. Inspection \cite{Fag86} and formal methods are generally shown to be effective \cite{HB95,Whe96}. Although inspection can, in principle, detect all types of errors in SRS, experience in conducting inspections on the SRS for the Wolsong NPP (nuclear power plant) SDS2 (shutdown system) \cite{AECL94} revealed that inspection is ineffective when verifying application-independent properties of large, complex, and evolving software requirements.
To leap these limitations, we decided to use formal methods as an activity in the verification process and fault tree analysis as an activity in the safety analysis. Safety-critical software process is composed of development process, verification process, and safety analysis process. The safety analysis process is an additional process which is not found in a conventional software process.
A software requirements specification is an artifact of requirements phase in development process. The verification process in requirements phase checks the correctness of software requirements specification, and the safety analysis process analyzes the safety-related properties in detail.
We classified properties to be verified into static properties and dynamic properties in the verification process, and we proposed verification methods for each property using a theorem prover, PVS. \textit{Static properties} are application-independent properties, and require that definitions and uses of variables, functions, and function groups are consistent. \textit{Dynamic properties} are application-specific properties and specify conformance between
software requirements specification written in formal specification language and program functional specification written in natural language.
We proposed a method to synthesize a software fault tree from software requirements specification for safety analysis process. A fault tree is one of the most classical and popular technique for safety analysis, but it does not provide a systematic construction procedure and applies mainly in hardware not in software. We proposed a fault tree synthesis technique based on templates.
All proposed analysis methods were applied into industrial software systems not toy problems. The shutdown system of Wolsong nuclear power plant was used for verification of static and dynamic properties. The reactor protection system of APR-1400, the Korean next generation nuclear reactor system, was used for synthesizing a template-based fault tree.
Our proposed methods support verification and safety analysis process in the requirements phase so that they support every activities in the requirements phase. And the application of the method could improve the quality and safety of a safety-critical software.
컴퓨터로 제어되는 안전성이 중요한 시스템의 사용은 계속적으로 증가하여 현재 여러 곳에서 발견할 수 있다. 항공 제어 시스템이나 원자력 발전소의 정지 시스템이 그 대표적인 예이다. 국내외 규제 기관으로은 이러한 시스템의 안전성 보장 요구 사항을 만족하고 있음을 엄밀하게 보일 것을 요구하고 있다. 예를 들어 결함 확률을 $10^{-9}$
이하로 유지할 것을 요구하기도 한다.
소프트웨어 개발의 여러 단계 중 요구 사항 단계는 소프트웨어 품질에 가장 큰 영향을 미치는 단계로 알려져 있다. NASA의 자료 \cite{Lut96}에 의하면 운영중인 소프트웨어에서 발견되는 문제점 중에서 약 $75\%$가 요구 사항에서의 오류가 원인이라고 한다.
품질이 높은 소프트웨어 요구 명세를 개발하기 위하여 다양한 방법이 제안되었고, 비용 대비 효율성 분석도 수행되었다. 일반적으로 인스펙션 \cite{Fag86}과 정형 방법이 효율적인 방법으로 알려져있다. \cite{HB95,Whe96}. 원칙적으로 인스펙션은 SRS에 존재하는 모든 종류의 오류를 찾아낼 수 있지만, 월성 원자력 발전소 제 2 정지 시스템을 검증한 경험에 의하면 \cite{AECL94}, 인스펙션은 분량이 많고 복잡하고, 계속적으로 변경되는 소프트웨어 요구 사항의 정적인 검사 조건을 검증하는데에는 비효율적임을 알 수 있었다.
이러한 한계점을 극복하기 위해 우리는 정형 검증 방법을 검증 프로세스의 행위로 사용하고, 고장 수목을 안전성 분석 프로세스의 행위로 사용하기로 결정하였다. 안전성 분석 프로세스는 일반적인 소프트웨어 프로세스에서는 존재하지 않는 추가적인 프로세스이다.
소프트웨어 요구 명세는 개발 프로세스 중 요구 사항 단계의 산출물이다. 검증 프로세스는 시스템에 소프트웨어 요구 명세의 올바름을 검사한다. 안전성 분석 프로세스는 안전성관련 속성을 자세히 분석한다.
본 연구에서는 검증 프로세스에서 검증하고자 하는 검사조건을 정적 검사조건과 동적 검사조건으로 구분하였다. 그리고, 각각의 검사조건을 정리 증명기 PVS를 사용하여 검증하는 방법을 제안하였다. 정적 검사 조건은 응용 시스템에 독립적인 검사 조건으로 변수, 함수, 합수그룹의 정의와 사용이 일관성이 있어야한다는 것이다. 동적 검사 조건은 응용 시스템에 의존적인 검사 조건으로 정형 명세 언어로 쓰여진 소프트웨어 요구 명세와 자연어로 쓰여진 프로그램 기능 명세의 일관성을 검사하기위한 검사 조건이다.
본 연구에서는 안전성 분석 프로세스를 위해서는 소프트웨어 요구 명세로 부터 소프트웨어 고장 수목을 생성해내는 방법을 제안하였다. 고장 수목은 안전성 분석 분야의 가장 고전적이고 인기 있는 방법 중 하나이다. 하지만, 체계적인 방법이 제공되지 않고 소프트웨어 분야가 아닌 하드웨어 분야에서 주로 사용되었다. 우리는 템플릿에 기반한 생성
방법을 제안하였다.
모든 제안된 방법은 작은 문제가 아닌 실제 산업계의 소프트웨어 시스템에 적용되었다. 정적 검사 조건과 동적 검사 조건의 검증은 현재 운영 중인 월성 원자력 발전소의 제 2 정지 시스템에 적용되었고, 템플릿 기반 고장 수목 생성은 현재 개발 중인 한국 차세대 원전 시스템인 APR-1400의 반응기 보호 시스템에 적용되었다.
우리의 제안된 방법은 요구 사항 단계의 모든 행위를 지원하기 위해 검증 프로세스와 안전성 분석 프로세스를 지원한다. 그리고 이 방법의 적용을 통해 안전성의 중요한 시스템의 품질과 안전성을 향상 시킬 수 있다.
