S3 boxes def

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

S3_generique_site_en

  1. Specification of the analysis goal: safety properties, test objectives, optimization criteria,…
  2. Formalization in HLL (High Level Language) by an application field modeler
  3. Automatic translation of the system  into an HLL model using a specialized translator (C, Ada, SCADE,…)
  4. 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) logo_certifiable-smart-solver

  • 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)
  • CBTC (Communication-Based Train Control System)
  • ERTMS (European Railway Traffic Management System)
  • Avionic air flow regulation systems

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).

Contact us