In this, the third and final, blog post on Signal Design Automation we will look at how Formal Verification and automation are used at Stockholm Metro to increase railway safety. The rail-based public transport system in Stockholm, Sweden is relatively complex and diverse with a combination of subway, light rail and heavy rail. It also [...]
We have now published a new date when we will run our popular webinar about Formal Verification. The date for the webinar is the 28th of April. Safety verification is vital for railway interlockings. During this webinar we will describe the general problem of safety verification and show that formal verification is the only method [...]
In a previous blog post, a playful concrete example was given to show off PSL's newly added support for IEEE 754 floating point calculations. We have tested the performance in real world industrial examples and in this blog post we will take a look at the floating point performance of PSL on a real world [...]
If you have read the first two parts of this series (Read Part 1 here and Part 2 here), then you know that verifying an interlocking that satisfies safety requirements is not an easy task to accomplish. Due to the huge size of the state space of the interlocking, neither manual methods nor testing will [...]
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 [...]
We at Prover are very happy to announce the release of version 4.0 of our model checker Prover SL CE (PSL). The most interesting new feature is support for IEEE 754 floating point calculations, so I will dedicate this technical blog post to floats with a concrete example of a floating point system which we [...]
We are happy to announce that CASCO Signal Ltd. (CASCO) and Prover Technology (Prover) have entered into a long-term agreement for the supply of Prover’s Signal Design Automation product suite Prover Trident. The initial focus is to further strengthen CASCO’s position as a leading supplier of signaling systems for China’s railway segment, by the use [...]
2017 an idea was born at Prover Technology, we wanted to create a forum for sharing experiences and best practices, and for networking. Our intention was to gather leading signaling management peers from all over the world to discuss the latest evolutions of design automation and formal verification– software technologies to automate design and verification [...]
The Tool providers that support HLL have now agreed on the content of the next published version of HLL. It will be a merge of the different dialects of HLL that exist today. One language for all Over the years tool providers have developed HLL in different directions in order to solve their particular needs and to [...]
