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

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

Last News

January 2019 Systerel Smart Solver: always faster

November 2018 First HLL forum