Static analysis and formal proof of systems and software
Systerel offers a range of industrially proven solutions using Model Checking based technologies for the static analysis and formal proof of systems and software. Systerel Smart Solver (S3), a SAT based analysis tool is central to these solutions.
A wide range of services
In conjunction with specialized translators and specific tools, S3 is able to offer a variety of services:
Static code analysis
Proof of safety properties – certification
Proof of user properties with counter examples analysis tools
Automatic test case generation (functional or structural)
Synopsis
Specification of the analysis goal: safety properties, test objectives, optimization criteria,…
Formalization in HLL (High Level Language) by an application field modeler
Automatic translation of the system into an HLL model using a specialized translator (C, Ada, SCADE,…)
Analysis of the system and creation of the results (proofs, counter-examples, scenarios, tests,…)
Benefits
Automated analyses and proofs
Analysis completeness
Exact modeling (no abstractions)
Compliant with certification processes
Dedicated team of specialists of the technology and tools
Functionalities
Static code analysis: absence of unspecified behaviors (OOB, UMR, OVF, DIV0), absence of unreachable and dead code
Proof of user-defined properties
Counter-examples analysis of falsified properties
Automatic test case generation (functional or structural)
Equivalence proof between specification and code, or between diversified codes
Languages: C (C99 with some restrictions), Ada (subset), SCADE (v5,v6)
Certifiable Systerel Smart Solver (cS3)
Certifiable analyses of the conformity of a system with a set of properties (safety, specification…)
According to the EN 50128:2011 norm, tool class T2 for SIL-4 systems
Based on diversification, sequential equivalence checking and a posteriori proofs verification
Industrial applications
Safety verification for a wide range of systems, including:
Railway Interlocking systems (relay-based and computerized)
Systerel Smart Solver is a powerful proof solution. It increases confidence in the security level of a system while considerably reducing the time and cost of validation.
Various measurements carried out on industrial-scale projects show significant performance gains in the validation of safety properties: validation activities that previously took several months to complete are now done in a matter of hours.
The application of Systerel Smart Solver on an industrial scale by major rail industry players (Hitachi, Alstom, RATP, SNCF, etc.), and the demonstration, in representative cases, of its ability to address the vast majority of interlocking systems currently deployed by SNCF for example, confirm the maturity of the implementation of formal verification for the development and deployment of operational interlocking systems.
For academic experimentations or prototyping needs, Systerel gives access to licences of the Systerel Smart Solver. Systerel provided such licences to the French national aerospace research center (ONERA).
