The digital software control system in nuclear power plants is a safety-critical system where reliable techniques must be applied to it in order to preserve safety in the whole system. Formal specification and verification technique are known to improve the safety of safety-critical system software.
Formal specification techniques especially allow the system to be clearly and completely specified in the early requirements specification phase. Formal verification methods can detect errors which can not be detected using the methods such as inspection, and safety analysis techniques. Since formal specification and verification methods can preserve safety in the whole system, recently there has been a great increase of researches and applications in the industrial field.
In this paper, we present NuEditor, an integrated specification and verification environment to perform both specification and verification of requirements specification written in NuSCR. NuEditor offer convenience of specification to specifier through check of syntactic error. Moreover, it can provide information about omitted or conflicted requirements, since NuEditor provide a functionality to preserve the completeness and consistency of the NuSCR specification. More complex system properties can be verified automatically using formal verification techniques by NuEditor. To implement automatic verification environment, we also propose translation rules for NuSCR into SMV.
To demonstrate the usefulness of our proposed NuEditor, we present a trip logic of BP(Bistable Processor) in DPPS(Digital Plant Protections System) RPS(Reactor Protection System) in nuclear power plant as an example system, which is currently being developed in Korea. When we specify a trip logic of BP, frequently occurring errors such as omission of input/output variable and logic are effectively identified. Verification using model checking and theorem proving is proven to be applicable and effective to check properties related to dynamic behaviors of system.
원자력 발전소의 디지털 제어 시스템의 소프트웨어는 safety critical system 이므로, 시스템의 안전성이 보장되기 위한 기법들을 필요로 한다. 특히, 정형명세 기법과 정형검증 기법은 Safety critical software의 안전성을 크게 향상시킬 수 있는 기법으로 알려져 있다. 정형명세 기법은 개발 초기 단계에서의 요구사항을 명확하고 완전하게 표현하여 줌으로서, 정형검증 수행을 용이하게 해준다. 정형검증 기법은 인스펙션, 안전성 분석 등의 통상의 방법으로 검출하기 어려운 오류들을 검출해 준다.
현재 개발중인 한국의 KNICS(원전계측제어시스템 개발사업단)의 DPPS(디지털 발전소 보호계통) 는 소프트웨어에 의하여 통제되는 safety critical system이다. 현재 개발 프로젝트에서는 DPPS의 안전성을 향상 시키기 위하여 요구사항을 정형 명세 언어인 NuSCR를 이용하여 기술하고 있다. 또한, 인허가를 위하여 기술된 요구사항 명세에 대하여 일정 수준의 분석 및 검증을 요구한다. 하지만 대상 명세 언어인 NuSCR의 경우 현재 자동화 도구가 부재하기 때문에 원자력 분야의 전문가 들이 명세하는 데 있어서 많은 시간과 노력이 소요된다. 또한 분석 및 검증을 하는데 있어서 한계를 가진다.
본 논문에서는 NuSCR를 명세하고 검증하기 위한 자동화 도구인 NuEditor를 제안하고자 한다. NuEditor는 명세 단계에 빈번하게 일어나는 오류들을 검사하여 기술의 편의성을 제공한다. 또한 추가적으로 일정수준의 완전성과 일관성 검사를 수행하여 누락되거나 상충되는 요구사항을 파악하는데 도움을 준다. 더 복잡한 시스템의 요구사항들은 NuEditor가 제공하는 정형 검증 기능을 이용하여 자동으로 분석될 수 있다. 또한, 검증환경의 자동화 구현을 위해 NuSCR을 SMV의 입력언어로의 변환규칙을 정립하였다.
DPPS RPS(원자력 보호계통)중에서 가장 중요한 논리를 수행하는 부분인 BP(Bistable Processor)의 트립 발생논리를 대상으로 하여 NuEditor의 유용성을 알아보았다. 예제 시스템을 NuEditor를 이용하여 명세하는 과정에서는 흔히 발생하는 누락된 입/출력 변수 및 논리를 파악하는데 효과적이였다. 그리고, 본 논문에서는 자동 검증 기능을 이용하여 정적으로 검사할 수 없는 시스템의 동적 행위에 관련된 요구사항을 검증하고 수정할 수 있는 가능성을 제시한다.
