The safety analysis of requirements is a key problem area in the development of software for hybrid real-time safety systems. Major obstruction of using formal methods for hybrid real-time systems in industry is the difficulty that engineers have in understanding and applying the quantitative methods in the abstract requirements phase. While formal methods technology in safety-critical systems can help increase confidence in the software, the difficulty and complexity of using them can cause other hazards. In order to overcome this obstruction, we propose a framework of requirements engineering for the hybrid real-time systems. It consists of a qualitative method for requirements specification, called QFM (Qualitative Formal Method), and a safety analysis method for the software requirements based on causality information, called CRSA (Causal Requirements Safety Analysis). The QFM emphasizes the idea of a causal and qualitative reasoning in formal methods to reduce the difficulty of specifying and validating the software requirements of hybrid safety systems. We use the qualitative formal languages, Compositional Modeling Language, and Causal Functional Representation Language in particular, to specify hybrid system dynamics and the required behavior respectively. The system behavior has been simulated by the Device Modeling Environment, and validated against the required behavior. CRSA can evaluate the logical contribution of the software elements to the physical hazards of systems without the subjective and ad hoc decisions of safety analysts, by using the causality information that is kept during specification by QFM. Using the Shutdown System 2 (SDS2) of Wolsong nuclear power plants as a realistic example, we demonstrate that the QFM provides a practical solution for requirements specification of HRTS, and that the CRSA is a systematic approach for safety analysis of HRTS software.
원자력 발전소 보호계통, 인공위성, 미사일 등에 탑재된 컴퓨터 제어시스템과 같이 비선형 연속성을 갖는 제어대상 시스템과 이산상태 변화에 의해 실시간으로 상호 작용해야 하는 시스템을 복합 실시간 시스템 (HRTS: Hybrid Real-Time System) 이라고 하며 그 안전성 보장이 필수적이다. 복합 실시간 안전계통 개발을 위한 정형기법 사용의 주된 장애요인은 기법의 인지적 어려움이다. 즉, 엄격하고 정량적인 정형기법을 이해하여, 요구사항 도출을 위한 대화수단으로 사용하기가 어렵고, 이를 추상적이고 정성적인 요구분석 단계에 적용하기가 어렵다. 안전계통 개발에 정형기법을 사용하고자 하는 이유는 안전성 제고임에도 불구하고 사용상의 어려움과 복잡도는 또 다른 위험을 초래할 수 있다. 이러한 문제를 극복하기 위해 복합 실시간 안전계통 요구분석과 안전해석 시 사용자의 인지적 부담을 줄여줄 수 있는 정형기법을 제안한다.
이 논문에서는 먼저 복합 실시간 안전계통의 요구사항을 명세하고 그 안전성을 분석할 수 있도록 인지적 요구분석 체계를 설명한다. 이 체계는 요구사항 명세를 위한 인지적 정형기법 (QFM: Qualitative Formal Method)과 원인결과 요구사항 안전성 분석기법 (CRSA: Causal Requirements Safety Analysis)으로 구성되어 있다. QFM의 특징은 요구사양 설계자와 분석자의 인지적 부담을 줄여주기 위해 인공지능 분야에서 연구된 정성추론, 특히 인과추론 이론을 정형명세에 도입한 것이다. 즉, 연속시간과 이산시간 속성을 복합적으로 가지는 실시간 계통을 표현하기 위해 정성적 정형 언어인 합성명세언어 CML (Compositional Modeling Language)을 사용하였고, 요구되는 기능요건과 안전요건을 표현하기 위해 원인결과 기능표현언어 CFRL (Causal Functional Representational Language)을 사용하였다. CML로 표현된 HRTS의 동작특성을 DME (Device Modeling Environment)를 이용해 시뮬레이션 함으로써 계통 상태의 원인결과 정보를 도출하고 이를 기능 및 안전 요건과 비교 검증한다.
QFM과 의미론적으로 통합된 CRSA는 고전적인 소프트웨어 고장수목 분석 분석기법 (FTA: Fault Tree Analysis)을 사용하지만 QFM에서 생산된 원인결과 정보를 활용함으로써, 이전의 소프트웨어 FTA 기법들이 가지는 분석자의 주관과 시스템 이해능력에 의존하는 단점을 보완하였다. 또한 QFM의 결과로 생산된 원인결과 정보의 활용은 소프트웨어의 논리적 결함이 시스템의 물리적 안전에 어떠한 영향을 주는지 추적할 수 있도록 하며 시스템 안전해석과 소프트웨어 안전성 분석을 연결시켜 주는 장점이 있다.
인지적 요구분석 체계의 기본 틀은 인지시스템공학의 목적-수단 조직단계 (Means-Ends Hierarchy) 개념을 바탕으로 하고 있다. 따라서 QFM과 CRSA는 기존 기법들이 가지는 입출력 중심 명세와 안전해석기법의 단점을 보완한 목표기반 (Goal-based) 명세 및 안전성 분석 기법이라 할 수 있다. 제안된 기법들의 효과를 검증하고 기존 입출력기반 기법과 비교하기 위해 산업현장의 실질적 예제로 월성 원자력 발전소 보호계통 요구사항 명세와 안전성 분석을 수행하였다.
