Fourth International ERCIM Workshop on Formal Methods in Industrial Critical Systems
This paper demonstrates the use of model checking based verification technology to establish safety critical properties for a railway control application. The verification technology is tightly integrated with the Statemate system of I-Logix Inc., USA. Key features of this technology are the powerful debugging capabilities and graphical entry for safety critical properties. This paper gives an overview over the verification environment and also highlights the design methodology that provides its base. In order to further enhance the verification environment we add Message Sequence Charts (MSC) to the existing tool-set. We show that MSCs can be effectively used in the requirements analysis phase of the design process. As a sample application serves a railway control system.