Our tools

Formal analysis of software

Formal analysis of software by CLEARSY

Formal analysis of software

CLEARSY proposes a new innovative analysis approach to establish with mathematical proof that all or part of a software are compliant with respect to a functional or a safety requirement.

This approach establishes a direct formal link between the source code of the software and the properties of the system that integrates that software. It is now possible to detect any kind of noncompliance that may have been introduced in the design phase: from the identification of algorithms during the system definition phase, up to their concrete realization, taking into account possible implementation specific constraints.

The formal analysis approach proposed by CLEARSY is complete: it is guaranteed to cover all possible functional behaviors, including as a matter of fact all system dysfunctions and failures that have not explicitly been discarded. This is the benefit of using a method based on mathematics and a property-based approach, instead of a case-by-case approach.

Industrial interest

The benefits of such a formal analysis numerous:

  • To consolidate and lay down the functional and safety requirements: to state explicitly what guarantees the system shall enforce.
  • To identify noncompliant behaviors: violations of properties that may have deep consequences on the safety or on the operation of the system integrating the software under analysis.
  • Recover initial reasonings: the original intentions of the system designers.
  • Lay down design choices: by finding their justification, thus providing a guarantee that the software under analysis is technically mastered.
  • Uncover useless or obsolete complexity nodes: to simplify the software for improved performance and functional features (the simpler the software, the larger the possibility to be well-behaved).
CLEARSY formal analysis of software

Flowsheet of the formal software analysis tool by CLEARSY.

Quickly providing concrete results

This method is pragmatic, quickly providing concrete results for the project. With the results obtained from previous applications, CLEARSY has reached the conclusion that the formal analysis of software presents a real gain both for the supplier of a product and its operator. The approach benefits from being used on products that evolve over time, or that are widely deployed, or that integrate options based on their use.

Commercial references

logo Alstom
logo RATP
logo SNCF Réseau
Logo New York City Transit