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 non compliant 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).
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
 |
 |
 |
 |
Link to this offer
Linked to this offer
Linked to this offer
- • Extension of Line 14 of the Paris Metro: over 25 years of reliability thanks to the B formal method
- • CLEARSY joins forces with The Neat Company to integrate the CLEARSY Data Solver validation tool into the Horizon track plan editor!
- • A certified version of ATELIER B is planned for 2024
- • Formal activities through the V cycle
- • CLEARSY will attend the ERTMS 2022 Conference
- • Formal methods in action in the railways
