The Analysis of Formal Methods for Applying to Vital S/W in Train Control Systems

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 the comparison of other formal methods, we choose the compromise method with Z (Zed) and Statechart formal language for applying to the train control system. Using Z is able to realize higher correctness in the requirement specification, and we propose the Statemate of the best solution in formal verification tools for the system modeling and verification.