Verification of a safety-critical railway interlocking system with real-time constraints

Ensuring the correctness of computer systems used in life-critical applicat ions is very difficult. The most commonly used verification methods, simula tion and testing, are not exhaustive and can miss errors. This work describ es an alternative verification technique based on symbolic model checking t hat can automatically and exhaustively search the state space of the system and verify if properties are satisfied or not. The method also provides us eful quantitative timing information about the behavior of the system. We h ave applied this technique using the Verus tool to a complex safety-critica l system designed to control medium and large-size railway stations. We hav e identified some anomalous behaviors in the model with serious potential c onsequences in the actual implementation. The fact that errors can be ident ified before a safety-critical system is deployed in the field not only eli minates sources of very serious problems, but also makes it significantly l ess expensive to debug the system. (C) 2000 Published by Elsevier Science B .V. All rights reserved.