Safety Requirements Specification and Verification for Railway Interlocking Systems

The integration of formal methods and requirements analysis increases the dependability of safety-critical systems. However it is still very difficult to obtain all of the safety requirements in practice, and formally construct the safety requirements model as well. In this paper, we propose an approach to capture safety requirements and formally describe them by classifying and developing safety requirements specification patterns. Our classification is a result of extracting safety properties from a variety of sources, such as interlocking tables and existing safety relevant functional requirements of railway interlocking system. They contain safety properties at analysis level and design level respectively. Furthermore, safety specification patterns based on the classification are used to formally describe and organize the safety requirements for formal verification. Finally, a tool called SRSV has been developed to enhance the process from deriving safety requirements to verifying. We applied it to the interlocking system at Mohe station in China, and the generated safety properties were then checked to hold by the verification tool.