Systerel’s ‘Formal Modeling and Verification’ Center of Expertise is one of the largest European teams in this field and has over 25 years of experience in the industrial implementation of formal methods.
Use of Formal Methods
Why use formal methods?
Which techniques for which challenges?
Model Checking with S3
Systerel uses Model Checking to verify the safety properties of artifacts in the system development process. It relies on models/translations in HLL and on the S3 proof engine.
B Method Software
Systerel uses the formal B method for the development of safety-critical software in an industrial context. This technique allows for proving that the software’s formal specification is consistent and that its code conforms to the specification
Data Verification with B OVADO²®
Systerel uses the formal method B OVADO²® to validate the configuration data of a system. This technique is based on verifying the compliance of each data set with predefined rules using the OVADO²® tool from RATP.
Event-B Method
Systerel uses the formal Event-B method to prove that a system meets safety properties. This technique relies on the RODIN platform, which Systerel maintains and develops further.
SCADE Modeling
Systerel provides consulting and expertise services related to the implementation of SCADE and its integration with other technologies.
HLL Language
Systerel has now been using HLL for many years in the formal safety verification of critical systems such as CBTCs, interlockings, logical control-command circuits, but also for the optimization of constrained systems.
Verification & Validation Tools
Systerel develops solutions using formal methods to increase quality and productivity in the areas of verification and validation.