For the next big advancement in the development of faster and more efficient transportation, the railway industry has to go through a digital transformation. For this, safety is critical. The solution? New, more efficient verification methods. Perhaps the most apparent safety verification method is testing, and indeed, it is still the backbone of [...]
Hopefully you have read part 1 on this blog, where I tried to convince you that traditional methods will not get you very far when verifying safety requirements for railway interlockings. This time my task is to convince you that formal verification will get you far. In fact, all the way. So what is formal [...]
The subject I am going to write about this time is not an easy one. I will try to explain why formal verification is good. In particular, why it is a good practice to use formal verification when verifying safety requirements on railway systems. The Verification Problem In order to make a convincing argument, I [...]
The formal language HLL (High Level Language) has emerged in recent years as a quite popular language for formal verification of safety-critical systems, especially in the railway signaling domain. This year marks the 10th anniversary of its conception. The history of HLL The language has its roots in the proof engine technologies developed by Prover in the 1980s (Stålmarck's [...]
If you are involved in designing and safety assessment of signaling systems, then the Signaling Design Automation Forum 2018 is something for you! Using Design Automation The conference will be focusing on Design Automation and Formal Methods, where leading Infrastructure Managers and suppliers from around the world (such as RATP, NYCT, SL (Stockholm Metro), Siemens [...]
We've all been there, waiting for the theorem prover to answer. Getting up for a cup of coffee, bugging a colleague... still no answer. This can be standard behaviour when doing formal verification. The requirements are difficult to prove, the system manages to escape into some dark corner not easily approached by the theorem prover. [...]
In my last post I wrote about how to write a decent specification on a quite general level. This time, I like to return to the topic, trying to be a bit more specific and tell you something about how we at Prover like to do things. In the Prover Trident Process, the specification of [...]
Involved in Designing and Safety Assessment of Signaling Systems? Then the Signaling Design Automation Forum 2018 is something for you! The Signaling Design Automation Forum is the event to embrace the latest evolutions of design automation – software technologies to automate design and verification for railway signaling systems. The conference will be focusing on Design Automation [...]
Back in March this year I wrote about a work package on formal methods and standard interfaces, led by the Swedish Transport Administration (Trafikverket, and part of the European Shift2Rail (S2R) Joint Undertaking. Since that time, the proposal for the overall project that includes this work package has been submitted and become approved, and the project started [...]
In the early days of railway history there were no interlocking systems. It was considered enough to have personnel at the train stations manually observing trains and operating signals. The need for automatic signalling eventually became evident: human beings tend to make mistakes, which can lead to serious accidents, and the capacity of railroads was [...]
