--- title: "SafeCap: Automated Verification of Railway Signalling" url: "https://www.systra.com/uk/expert_insights/safecap-automated-verification-of-railway-signalling/" type: expert_insights date_published: 2018-09-28 date_modified: 2023-09-14 schema: @type: WebPage language: en-GB word_count: 1040 reading_time: 6 min canonical: "https://www.systra.com/uk/expert_insights/safecap-automated-verification-of-railway-signalling/" featured_image: "https://www.systra.com/uk/wp-content/uploads/sites/11/2018/09/safecap.png" type-insight: - Optimising the Journey --- # SafeCap: Automated Verification of Railway Signalling **The increasing complexity of modern railway signalling systems, both in terms of geographic coverage and of functionality, poses a major challenge to safety verification. The challenge is compounded by the scarcity of skilled resources in proportion to the number of projects underway.** Automation has long been proposed as a means of addressing this challenge (for example Section 4.5.1 of Network Rail standard NR/L2/SIG/11201/Module B11), though implementation of a practical, cost-effective automation process has frequently proved elusive. SafeCap brings a practical approach to automated verification, using computer science formal methods to enhance efficiency and accuracy whilst integrating with existing testing processes. Formal methods are a family of mathematical techniques for the specification, design, analysis and verification of software and hardware systems. They have been successfully used in multiple industries including transport, defence, telecommunications and nuclear power. Recent advances in formal methods make it possible to successfully apply them in a range of complex applications. Developed through collaboration between SYSTRA and Newcastle University, the SafeCap signalling verification module applies formal methods to signalling data in its native format, allowing data to be quickly and efficiently checked for compliance with pre-defined signalling principles. ![safecap](https://www.systra.com/uk/wp-content/uploads/sites/11/2018/09/safecap-1024x566.png) ### Verification with formal methods Traditional verification processes, both manual and automatic, test that a signalling system behaves as expected in pre-defined scenarios – the greater the number and variety of scenarios, the more comprehensive the testing. However, for all but the simplest systems, it is not possible to test every possible scenario. Formal methods take a different approach, using logic to reason about complex systems to construct a rational proof that the system will always conform to certain safety properties. A railway signalling example of such a safety property is that the commanded position of points never changes when a train is detected to be on those points. A key advantage of the formal approach is that, unlike traditional testing, it is fully comprehensive for the safety properties that it is verifying: there is no risk of missing a scenario where the property is violated. Furthermore, formal methods can be automated, enabling verification to be carried out much more quickly and cost effectively than by using traditional manual testing processes. Mature, automatic prover tools to construct the logical arguments used by formal methods, are already widely available, though so far, their application to railway signalling has been limited. ### The SafeCap Approach A key reason for the limited uptake of formal methods in railway signalling has been the high upfront investment needed before any benefits can be realised: - Training of signalling engineers in formal notation. - Specification of signalling data and principles in this notation. - Licence fees for software tools. A further reason has been the limited scalability of early approaches to formal methods, making them unsuitable for the complex railway layouts where they are most needed. SafeCap overcomes these drawbacks through an evolutionary approach to the application of formal methods based on the (highly scalable) method of analysing data as a state transition system. Data is verified in its native language, such as Solid State Interlocking (SSI) Geographic Data Language (GDL), with which signalling engineers are already familiar. Rather than attempting to verify every signalling principle from the outset, initial deployments of SafeCap verify a targeted subset of frequently used principles. The automated approach can be applied alongside existing data preparation processes, delivering benefits through enhanced safety assurance and reduced re-work (through early identification of errors). Looking to the future, it is planned to expand the range of signalling principles verified so as to enable more potential errors to be detected early and automatically in the signalling data preparation process. It is also planned to develop a safety case to support the use of SafeCap as an alternative to some testing activities, thereby enabling further benefits in terms of reducing the project costs and timescales associated with signalling testing activities. ### Practical Results The practical application of SafeCap has focused on SSI GDL data as there is a large repository of signalling data, including several non-operational data sets with known errors in this language, on which to trial the approach. These trials have demonstrated that the approach works in practice by finding not only seeded errors and known errors (in non-operational data sets), but also errors (in non-operational data sets) of which those conducting the trials were unaware. The types of errors detected included those that, if in service, would allow points to move under trains as well as those that would allow signalling routes to be set/unset when is potentially unsafe to do so. The total process of verifying a dataset takes only a couple of days, including manual configuration of the tool and production of a commentary on the results. This makes it feasible to carry out verification quickly using a SafeCap and cost effectively throughout a project. The challenge of ‘false-positives’ (reported violations of signalling principles where none exist) is addressed through alignment of safety properties to data structures and use of goal structured notation to demonstrate that high level signalling principles are satisfied. SafeCap is a practical approach to the automatic verification of signalling data using computer science formal methods alongside existing data preparation processes. Co-developed by SYSTRA and Newcastle University, SafeCap has been shown to work effectively on complex real-world signalling data (50-100 routes) for SSIs (and hence also SSI derived interlockings). It has shown that it can quickly and efficiently find errors that, if they were in service, could lead to serious accidents. The formal rigour of mathematical analysis allows SafeCap to conduct complete analysis of the signalling system under development more comprehensively than is possible with manual testing. The practicality of the approach is in working alongside existing processes to reduce re-work and enhanced safety assurance. In the long term, it has the potential to deliver further benefits by completely replacing some manual testing activities with automated processes. Being automated and extremely scalable, even the most complex layouts can be verified extremely quickly. Watch [Formal Signalling Verification In SafeCap Demo](https://www.youtube.com/watch?v=rLc5PhWGMik) [JOIN OUR COMMUNITY](https://www.systra.com/uk/register/join-our-community/)