Application of statecharts and table methods to formal specification of the NPP trip function requirements원자력발전소 트립기능 요건의 정형적 명세를 위한 Statecharts와 테이블 방법 응용에 관한 연구
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.