This paper presents the results of study which develops the formal specification of the trip function requirements of SDS2 that is a safety critical system using an integrated formal approach that combines the statecharts and the table notation methods.
A visual formal notation, statecharts, is used to specify the requirements of the simplified SDS2. As background, the statechart approach to specifying requirements is reviewed. A table notation method is used to cope with the limitation of the statecharts. A table notation editor is designed to provide the automatic checking of the correct usage of the variables and to verify the correctness of the computational parts of the requirements. The developed specification is executed graphically using a simulator to ensure that it captures the intended behaviors of the system. The formal specification is analyzed statically for syntactic correctness and dynamically for potential errors. It is found that the formal specification makes it easier to detect incomplete specifications, specification errors or inconsistencies at an early stage.
In conclusion, it is believed that a great increase in confidence in the system can be obtained by the use of formal specifications at early requirements stage of the software life cycles.
본 논문에서는 Statecharts와 테이블 표기 방법을 결합한 통합된 정형적 접근 방법을 이용하여 원자력 발전소의 트립 기능요건에 대한 정형적 명세를 개발하고 Statecharts가 지니고 있는 단점을 극복할 수 있는 방법을 제안하였다.
단순화된 트립기능 요건을 기술하기 위하여 가시화된 정형적 표기 방법인 Statecharts를 사용하였다. 또한 복잡하고 긴 계산 요건을 기술할 때 표현식이 복잡해지고, 표현식의 정확성을 검증하지 못한다는 Statecharts의 단점을 극복하기 위하여 테이블 표기 방법의 사용을 제안하였다. 테이블 표기를 위한 편집기를 설계하였으며, 이러한 편집기를 이용하여 변수의 정확한 사용 및 계산 부분의 정확성을 자동으로 검증할 수 있는 기능을 제공하였다. 이렇게 검증된 계산부분의 명세가 Statecharts의 툴인 STATEMATE 언어에 적합한 형태로 자동으로 변환될 수 있는 기능도 함께 제공하도록 설계하였다. 개발된 정형적 명세가 요구된 기능을 정확하게 포함하고 있는가를 검증하기 위하여 시뮬레이터를 이용하여 명세를 실행하였다. 또한 정형적 명세의 의미적 정확성과 잠재적 에러를 발견하기 위한 분석을 수행하였다.
본 연구를 통하여 정형적 명세 방법을 사용함으로서 명세의 불완전성, 오류 혹은 불 일치성 등을 설계 초기 단계에 용이하게 발견할 수 있음을 확인하였다. 결론적으로 소프트웨어 개발 주기의 초기 요건 단계에 정형적 명세 방법을 사용함으로서 시스템의 높은 품질보증을 가져올 수 있다는 확신을 갖게 되었다.
