Model Checking: Formal Modeling and Verification

Model Checking: Formal Modeling and Verification

Model Checking is a Formal Safety Verification method in which tools are used to analyze a model of a system in order to verify if it respects some safety properties. The analysis is performed by exploring every possible evolution trace of the system1, verifying that the properties hold on these traces.

Modelling the Code

The first task in a Model Checking solution is to obtain a model of the system that has to be analyzed. This model has to be expressed in a Formal Language with well-defined syntax and semantics such that a Model Checking toolset is able to analyze it without ambiguities. This is the Formal Model of the system.

Model Checking is usually seen as a very pragmatic and light-weight approach. It does not cast any requirement on the development process of a system, but rather hooks at some later stage of this development to use some artifact (design, code …) to automatically translate it into the Formal Model.

Modelling the Specifications

However it is also possible to manually develop the Formal Model from the informal specification of the system in a diversified track of the development process. With such an approach, the Formal Model takes a new role and can serve many other purposes than only Formal Safety Verification using Model Checking.

A Model as a Reference

First, this Formal Model can serve as a reference Formal Specification. This unambiguous specification becomes a blueprint for the main development process. It is a reference for the functionalities that have to be implemented in the software part of the system. As such, it is a support for discussions with the supplier in charge of developing this system. In this regard, a clear and complete documentation of the model is of utmost importance.

A Model as a Digital Twin

If the model checking toolset possesses simulation capabilities, and if the formal model contains a sufficient level of details, it becomes a Digital Twin. It can be used as a demonstrator of the functionalities of the system by running scenarios and observing the behavior of the model. This represents an additional mean to support discussions with the supplier. It is also a powerful tool to investigate the effects of changes in the specification on the functionality of the system. This Rapid Prototyping capability of the formal specification helps in the maturation phase of the system.

The Digital Twin can also be used to develop and mature the test suite that will be used for the Functional Validation of the developed system. The tests are initially run on the Digital Twin and any issue can be addressed at a very early stage of the development process. In a second phase, the test suite is run on the supplier’s system to verify its functional behavior.

A Model for Safety Properties

The main use of the Formal Specification is as the Formal Model of the system to support Formal Safety Verification. Using a Model Checker, safety properties can be analyzed on this model. The outcome of these analyses is either that a given safety property holds for every possible traces of the system model, or the Model Checker exhibits a scenario that shows a violation of the property.

Investigating the violation scenarios enables to correct the model, and thus mature the Formal Specification of the system at an early stage of the development process. In a first phase, where violation of the safety property occurs, this tool is used as a debugger of the specification. Once all the safety critical bugs have been fixed, the tool can be used to prove that the properties hold and bring evidence of the system safety for an EN50128 certification.

Model and Product Compliance

The system safety evidence brought by the Model Checker holds on the Formal Model. There are several approaches to claim that this safety evidence also applies to the developed system. The simplest is to consider that the development process of the supplier is sufficient to insure the compliance of the obtained system with the Formal Model acting as a Formal Specification.

The Back to Back Testing technique is a more formal approach to support this claim. Test cases are automatically generated using the Formal Specification in order to maximize some structural coverage criteria. The test cases are then run on both the Formal Specification and the supplier’s system to check that they behave identically. To be able to apply this method, it is necessary that the Formal Specification is complete, totally unambiguous and contains no abstraction.

Finally, if such a complete Formal Specification has been developed, it could be used to automatically generate the code of the application.

Systerel Smart Solver (S3) Model Checking Solution

Systerel develops a Model Checking Solution called Systerel Smart Solver (S3). This toolset is based on the HLL formal language developed and maintained by the HLL Forum, a consortium composed of RATP (the Paris metro authority), Systerel and Prover Technology. It is built around an EN50128:2011 T2 Certified HLL Model Checker able to conduct the safety analyses of SIL4 critical systems. It also contains an HLL documenter creating high quality HTML documentation of an HLL model, and an HLL animator able to simulate an HLL model to perform functional investigation and validation.

The B2BT tool can be used for generating Back to Back test suites and the HLL animator to run these tests.

The S3 toolset is used extensively to perform the formal verification of a number of railway interlocking systems, but also for several CBTC systems. In these solutions, the Formal Model is obtained with an automatic translation from the code of the supplier’s system.

S3 is also currently used to investigate the safety of the Level 3 hybrid algorithm of the ETCS norm. The Formal Model of the L3H algorithm, together with that of the L2 ETCS, the underlying interlocking and the asynchronous communication layers between these are modeled directly in HLL from the informal ETCS specification. This Formal Specification of the L3H algorithm is then analyzed by S3 to determine if it respects a number of safety properties.

The B2BT tool is used in an interlocking project to verify that the implementation of the system is correct with respect to a Formal Model obtained from a diversified track.


  1. In practice the exploration is not done on every possible trace because there are usually an infinite number of these. However the analysis mechanism insures that it is equivalent to a complete trace exploration.