PSL – Best-in class Formal Verification performance

Our model checker PSL has taken significant performance leaps compared to its predecessors and previous generations, for many applications lack of performance (i.e. long running times) of the verification tools is no longer a viable argument against using formal verification. Recent evaluations performed by our customers confirms that the current PSL not only outperforms earlier versions, but also that it is way ahead of its competitors. These evaluations have been done on industrial implementations of rail control software and embedded systems from avionics and automotive applications.

These performance leaps have been made possible by the implementation of improved algorithms that make better use of the multicore architecture of modern computers. A major performance improvement is also related to the modelling of IEEE 754 floating point calculation, which not only reduces computing time but also improves the precision compared to SMT-based solvers like the predecessor of PSL.

These improvements have drastically increased the number of systems that are in comfortable reach for formal verification, and in many cases, performance is no longer a concern. We can however expect that there will always be problematic cases, regardless on the advances of the performance of formal verification tools such as PSL. To deal with these problems one has to look at how systems are developed and verified, to address this Prover supplies expert verification and design services as well as a range of formal verification and design automation tools, within the Prover Trident product range.  These tools greatly simplify the verification tasks in development of rail control solutions such as interlocking, CBTC zone controllers, ETCS radio block centrals and car-borne controllers.

To support efficient verification of software for more general embedded systems, Prover is working with leading suppliers of model-based design tools that integrate PSL. A key application of PSL in this context is automatic generation of test-cases to meet specific code coverage measures (e.g. MCDC), something that can be very demanding for the verification performance due to the complexity of the code and the high number of test cases that are required.  

A key take away from Prover’s extensive work in supporting the rail control supply industry is that it always pays off to consider the verification task and the corresponding safety requirements from the very start of the development and design process. This ensures verifiability in the end and facilitates the overall development process by making the formal verification tools available not only to verification experts, but also to the software designers.  

We are continuously working on improving PSL and are expecting a new leap in performance to come with the introduction of AI guided proof strategies. You can read about the initial results of this in our previous post.