We plan to offer a small number of “mini tutorials” on the morning of Tuesday 4th June, before the main conference starts at lunch-time that day. As details are confirmed they will be added to this page.
SafeCap is an approach to formal verification of signalling interlockings that uses static proofs based on first order logic and set theory. Geographic interlocking configuration data is treated as a computer programme and transformed into a transition system. A schema, entered as a pictorial representation of the railway layout, expresses the topological relationships between signalling elements in logical form. In the context of the schema, the SafeCap uses multiple prover tools to automatically verify that specific safety invariants are upheld for each possible step of the transition system. These safety invariants express, in formal notation, the signalling principles that ensure the safety of train movements.
SafeCap ensures fully automated verification in which the input data is read in a standard railway industry format, such as the Solid State Interlocking (SSI) Geographic Data Language (GSL) used in UK railways and all over the world. Diagnostics are expressed in terms typically used by signalling engineers. This makes it easier to integrate SafeCap verification into the existing industrial development processes. SafeCap has proven itself effective in analysing several real-world SSI data sets and identifying errors in such (not in service) datasets. The approach is scalable, it dramatically reduces the rework cycle, decreases the overall cost of development, and improves the quality of signalling.
This tutorial will outline the architecture of the SafeCap toolset, explain how the verification is conducted, discuss our experience in applying SafeCap for verification of large datasets from the UK railway and demonstrate how real-world interlocking data is verified using SafeCap.
Starting with a pre-drawn schema and data set with seeded errors, the attendees will learn how to use the SafeCap tool to automatically identify and correct these errors. They will first learn how to express signalling principles in terms of simple safety invariants that can be proved directly. They will then progress to more complex cases whereby proof of one safety invariant is dependent on proving one or more other invariants.