| Title |
Applying Methodology for the Safety-Critical S/W Development of Railway Signaling with the Z and Statechart Formal Method |
| Authors |
조현정(Jo, Hyun-Jeong) ; 황종규(Hwang, Jong-Gyu) ; 윤용기(Yoon, Yong-Ki) |
| Keywords |
열차제어시스템;정형명세;정형검증 Zed ; Statechart |
| Abstract |
Recently, many critical control systems are developed using formal methods. When software applied to such systems is developed, the employment of formal methods in the software requirements specification and verification will provide increased. assurance for such applications. Earlier error of overlooked requirement specification can be detected using formal specification method. Also the testing and full verification to examine all reachable states using model checking to undertake formal verification are able to be completed. In this paper, we propose an eclectic approach to incorporate Z(Zed) formal language and 'Statemate MAGNUM' which is formal method tools using Statechart for applying to the railway signaling systems. |