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

 

Contact us