Formal Verification is the act of mathematically proving that a system respects some properties under a number of hypotheses. When such a property is proved to hold, it means that it is impossible to find an input scenario satisfying the hypotheses in which the system would falsify this property.

Systerel Smart Solver (S3) is a formal verification solution able to perform a proof of the safety of a critical system after its design (i.e. a posteriori). This solution, combining a specialized modeling language (HLL) with a SAT-based symbolic model checker, has shown to be particularly efficient in handling industrial-size critical systems coming from various domains such as railways or avionics.

Front-end translators exist for the Scade®, C, and Ada languages. For domain or customer specific languages, custom translators are developed.

Furthermore, the use of a combination of ad-hoc techniques (translation diversification, sequential equivalence checking, and a posteriori proof verification), together with the application of strict processes for the development of the S3 tools, allows to build custom formal verification solutions satisfying requirements of trustworthiness and certification according to some standard.

Using a formal safety verification solution brings numerous benefits to a development process:

The solution is a powerful debugger, giving a high momentum to a development process by dramatically shortening the generation / verification / correction cycles.
A formal safety verification is intrinsically complete, it will search for every possible falsifications, whereas human-defined test campaigns and reviews are usually sample-based and incomplete.
It clearly identifies the complete list of assumptions upon which the safety of the system relies.
A formal verification solution allows for a reduction of the testing and review efforts.
A number of standards highly recommend the use of formal verification to address the safety of a system (EN-50128 or DO-178C).
It is able to address the verification of the safety of a system taking into account failures, asynchronism, latencies, or other timing specificities between parts of a system that are usually beyond reach of traditional test-based verification solutions.
The use of formal verification in the verification of a system sends a strong and positive message to the market, and is sometime even a requirement for some customers.

S3 formal safety verification solutions are routinely used in assessing the safety of systems instantiated by data, such as IXL systems instantiated by railway track layouts. In these solutions, specific constructs of the HLL modeling language are used to capture the set of safety properties and environment hypotheses independently of any track layout. Latter, when assessing the system for a specific track layout, this GSS is automatically instantiated using the data corresponding to this layout. The instantiated is then analyzed by S3 to show that it respects the instantiated safety specification.

Using a comprehensive methodology to build the GSS from Safety Hazards, an S3 formal verification solution is thus able to unambiguously and automatically show the safety of instantiated systems with a trustworthiness complying with the EN-50128 requirements cast upon the T2-class of verification tools.

The three following posts expand on those concepts:

For commercial information and contact see the S3 product page.

Commentaires