What is new in Prover PSL 6.0? 

Reachability obligations – a new way to strengthen verification 

Prover PSL 6.0 introduces reachability obligations, a new type of verification check that complements traditional proof obligations. This feature allows you to verify whether specific states can be reached in your model, helping to refine system validation and efficiently identify edge cases. (Requires an add-on) 

HLL and sHLL simulation in Why tool 

Now, you can simulate HLL and sHLL models directly in the Why Tool. This integration enables step-by-step execution, making it easier to debug, analyze counterexamples, and validate expected behaviors — all within a unified environment. (Requires an add-on) 

Enhanced proof analysis with coverage and profiling 

Prover PSL 6.0 introduces two new analysis options for greater proof transparency: 

• A proof coverage analysis to identify which parts of your model are covered during verification, allowing you to optimize proof efficiency. 

• A profiling and performance optimization feature to gain insights into computational bottlenecks by tracking solver workload distribution. 

Greater flexibility with -move for softening constraints 

A new command-line switch allows you to dynamically move constraints, proof obligations, and other model elements between different HLL sections. This flexibility helps refine proof strategies and understanding of your model without modifying the core model structure. 

With Prover PSL 6.0, you gain enhanced debugging, deeper proof coverage insights, and improved solver performance—all designed to push your formal verification process to the next level. 

Upgrade to Prover PSL 6.0 today and elevate your formal verification process!

Inlägget Prover PSL 6.0 released – Reachability obligations along with HLL and sHLL simulations are new features dök först upp på Prover - Engineering a Safer World.

We have also introduced a new kind of parallelization of the powerful model checking strategy IC3, leading to substantial reductions in proof times. We saw runtime reduction from 111 seconds to just 1 second in one case, and an average speedup factor of 3.2 on other cases we measured. 

We are proud to provide you with the best tools possible. Please let us know what you think when you have tried Prover PSL 5.10. 

Inlägget Prover PSL 5.10 is here – faster than ever! dök först upp på Prover - Engineering a Safer World.

We are proud to announce that Prover Certifier has now been certified by TÜV NORD as a CENELEC EN 50716-compliant T2 tool for SIL 4 applications. This means that it fulfills the toughest requirements for verification and validation tools for safety-critical systems with railway applications in the European Union. The rail and metro industry is moving to this new standard, which is replacing the way-side standard EN 50128 but also covering rolling stock applications.  

EN 50716 is a clear improvement over EN 50128. Model-based development and verification is encouraged more than before: “Models can also reduce the need for certain activities, particularly when using formal proofs.”. Formal Methods are now highly recommended for all kinds of software. 

With the release of version 1.4, we meet the complex requirements of the rail and metro domain. Besides introducing the new norm compliance, several improvements have been included in this release. Prover Certifier continues to be EN50128-compliant as well. 

Inlägget Prover Certifier now EN 50716-compliant T2 tool for SIL4 applications dök först upp på Prover - Engineering a Safer World.

Rail and metro managers all over the world are currently struggling with the same challenge: to move from a drawing-oriented view of data to a modern approach of structured data in databases. Everyone is asking the same question: how can we ensure that the data we put in those databases is correct?

When data checking consisted of carefully reviewing a drawing, it was obvious what had to be done: the drawing must agree with reality and be clear enough to avoid misunderstandings. When approved, the drawing would be the basis for construction. Everyone who needed the data would look at the same drawing and therefore have exactly the same view as the reviewer had when the drawing was approved.

With structured data it is a different story. The data is not represented as a drawing but stored in a database. Reviewing it requires some way to retrieve and visualize the data, and it cannot be ensured that all consumers of the data will have the same view as the reviewer. The process also raises important safety concerns: can we trust the tools that the reviewer uses to visualize and approve the data?

Formats such as RailML have been put forward as standards for data exchange between computer systems. RailML does its job, but being based on xml, RailML files are hopeless for humans to review.

We therefore designed LCF. It is a data exchange format that can be read by both humans and machines. It was designed to fulfill some important criteria:

• Pure text – allows simple trusted software to be used for reading on screen or printing.
• Well defined – enables computer interpretation without ambiguity.
• No clutter – makes it easy for humans to read.
• Compact – saves the reviewer from getting lost in thousands of lines.

So why are we giving this away? Well, the purpose of a data exchange format is to exchange data, and as such it needs to be available to everyone. We look forward to a world where lots of tools speak fluent LCF with each other. With trusted structured data, formal methods will thrive, and the benefits of formal methods to automate and digitize rail control systems are what we truly care about.

Inlägget LCF – For data exchange between humans and machines dök först upp på Prover - Engineering a Safer World.

We established the concept of Prover Trident quite some time ago. The idea is simple: divide signaling software production in three phases.

1. Formal specification. Capture your signaling design principles in formal logic.
2. Formal development. Use your formal specification and your configuration data to build a model of a signaling system. Investigate it using simulation and verification and finally generate revenue-service ready code from the model.
3. Formal sign-off verification. Use an independent program to formally verify that all safety requirements are fulfilled and generate the safety evidence.

To aid the second phase we developed Prover iLock, and for the third phase we developed Prover Certifier. But we never offered any product for the first phase, until now, although we always stressed that the first phase is where you spend most of the time. Ironic, indeed. There is a simple explanation why it took so long for us to understand the importance of providing a good development environment. Formal specifications are written in plain text files, and there are lots of text editors out there already. Creating formal specifications requires a lot of thinking, but producing the file itself is easy, when you have decided what to write.

However, when we investigated more thoroughly how users spend their time, it was clear that the process of writing formal specifications could be simplified a lot. When a specification grows large, it becomes increasingly difficult to remember what is already in there. Therefore, it becomes increasingly important with good support for navigation, to find which functions have been implemented already for a particular object and how they are defined, to understand where a certain function is used, to find dead code, et cetera. Specification can consist of hundreds of files for complex applications, so all kinds of help in finding things and getting an overview of what you have is appreciated. We created Prover Studio to provide all this, as well as on-the-fly syntax checks of more advanced immediate semantic checks that help discovering errors early.

During formal specification writing, Prover iLock is repeatedly used to check the specification and to try it on concrete examples. It is quite common to find an error in the specification by using Prover iLock’s simulator or code viewer, for example. In such cases, it is convenient to be able to quickly open the relevant file and find the line that needs to be changed. To make it possible to open the relevant piece of specification from Prover iLock we need to provide our own editor and integrate the tools.

The first version of Prover Studio was realized as an extension to Visual Studio Code. Our users told us that Prover Studio makes a great difference already. We intend to keep Visual Studio Code as the framework for Prover Studio’s editing and navigation capabilities, but also expand Prover Studio beyond what Visual Studio Code can offer, with features such as graphical representation of logic.

Inlägget Introducing Prover Studio dök först upp på Prover - Engineering a Safer World.

Inlägget New webinar on Signaling Design Automation dök först upp på Prover - Engineering a Safer World.

Inlägget Time to start offering AI-tuned proof tactics to the world! dök först upp på Prover - Engineering a Safer World.

Inlägget Automated signaling systems design using Prover Trident dök först upp på Prover - Engineering a Safer World.

In this series of three blog posts on the subject we call Signal Design Automation, we will take a look at the reasons for this situation, present a solution and finally look at a case study where a Signal Design Automation process has been successfully applied in a real-life project.

Expectations and challenges in rail control projects

The successful delivery of a rail control system should meet the following typical expectations from the Infrastructure Manager:

• Improved interoperability and reliability, supporting system upgrades
• 1st delivery of the system shall be on time and have the correct functionality
• Efficient safety assessment for guaranteed safety
• Reduced life-cycle cost
  • Individual sub-systems should be separated with clear interfaces, providing flexibility in extending the overall life cycle
  • Support for change of requirements and functionality over time

Unfortunately, this is often quite far from the reality, and Infrastructure Managers (IM) are instead faced with signal modernization projects that:

• Requires multiple deliveries before the correct functionality can be demonstrated
• Safety Assessment is time consuming and largely done at late, critical stage in the rail control project
• Exceeds budgets and are delayed
• Locks the Infrastructure Manager to the same vendor for a long time, making maintenance and upgrades costly

In our experience, there is a number of root causes to this situation, both at the Infrastructure Manager side and on the supplier side. Naturally, suppliers may not benefit from delivering systems with open interfaces between sub-components and, if they are not required to do otherwise, they will happily stick to proprietary systems, enabling the supplier to dictate the conditions when the Infrastructure Manager is looking for an upgrade or component replacement. Here the Infrastructure Managers must drive the shift to industry standards and open interfaces and indeed there are initiatives in this direction, such as EULYNX, in which thirteen European Infrastructure Managers are working together to define standard interfaces for interlocking systems. 

Meeting the expectations in rail control project delivery

A key factor to success in any project is that the stakeholders can agree on the requirements, i.e. what is to be delivered, and that it is easy to validate that a delivery meets the requirements. In many tender specifications, the technical requirements formulated by the Infrastructure Manager are kept vague. Either as a deliberate strategy to give the supplier freedom to bid with the most cost-efficient solution, or since the requirements, and their importance, are not fully understood by the procuring organization.

A big risk with this approach is that there are a lot of implicit expectations and requirements that are not communicated with the supplier, and in the end the users may not get the system they wanted, even though it fulfills all the specified requirements. Without clear requirements it can also be difficult to understand the impact of different design solutions until the system is close to completion, at which time changes can be very costly. On the other hand, if the supplier can present the Infrastructure Manager with a clear specification, where functionality can be demonstrated with early prototyping at the start of the project, the chances of agreeing on the requirements and succeeding with the project are greatly improved. 

The other option is for the Infrastructure Manager to take control of the requirements and clearly specify, already at the tender stage, exactly what is expected of the system. Then it also becomes natural to require that the systems make use of open interfaces, addressing the issues of vendor-lock in and high cost of upgrades during the life cycle. And it works the other way around too; if you already have clear definitions of the system interfaces, then it becomes natural to provide clear requirement specifications for the overall system as well.

Clearly defined requirement specifications also pave the way for automation, as the step to formalize, or implement, them in a way that can be interpreted by automation tools will be small. The coding, functional testing and safety verification that turns the specifications into revenue services software can then be done automatically from simple application configurations.

A high level of automation means that it will be less costly to implement and evaluate the impact of changed requirements and increases the chances of getting the functionality right at the first installation. The use of automated, formal, safety verification, addresses many of the issues around the safety assessment in traditional development processes and can be applied throughout the development. Finally, a Signal Design Automation solution need not be vendor specific, and thus can further help avoiding vendor lock-in, especially if it is combined with the use of standardized components and interfaces. 

Formal Verification, a key to success in your rail control project

Formal Verification is a method to prove with 100% certainty that a system fulfills a given set of safety requirements. In practice this verification is automated, using computer programs that implement mathematical algorithms performing the proofs. Formal Verification is a key component to maximize the level of automation in the delivery of rail control software, as it can remove many of the manual safety review tasks typically used in traditional safety assessment processes. It is also the only manageable way to deal with the safety verification of more and more complex systems, without risk of losing the confidence in the system safety, or accelerating the verification costs and delivery times.

If you want to know more about Formal Verification you can study our recorded webinar here.

Inlägget More efficient rail control projects using signaling design automation (SDA) dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Major releases of PSL and Prover iLock dök först upp på Prover - Engineering a Safer World.