CLEARSY has developed and certified the CLEARSY SAFETY PLATFORM (CSP), a solution to develop safety critical real-time embedded systems certified up to SIL4. CSP provides a framework, based on the formal method B, to guarantee software-level safety properties. This framework includes a dedicated IDE, a detailed documentation and application examples.
The safety properties of the application are formalized in dedicated specifying modules, possibly including environment behavior. The modules also embed the software implementation of their specification. Thanks to the B method, such implementations can be formally proved to comply 100% with their specification. The CSP includes a library, also developed in B, providing the elements to express rich safety properties on software execution. In particular, timing properties can be formalized and proved.
The CSP IDE provides a fully automatic dual compilation process that generates a binary executable and uploads it on the CSP platform. This executable is guaranteed to execute faithfully the developed software or to fall back to a stable vital state, as soon as the conditions of a safe execution cannot be guaranteed.
Combining the B Method assurance on software development and the CSP assurance on compilation/execution, CLEARSY has built a complete software development framework from high-level safety properties to low-level on-board execution.
By adopting the CSP platform, the developers are relieved from the burden of handling hardware failures and focus their effort on the specification of the desired functionalities and safety properties and on the design of a solution that realizes this specification. The remaining steps are fully automatic and taken in charge by the certified tools and by the certified vital processing unit CSP.
CSP development framework:
- Certified software development
- Certified compilation process
- Certified execution
- Generic certificate and rules to apply for the environment
This is a big step forward extending the B method paradigm: “Assigning program to meanings”.
“Assigning safe processing to meanings” is a result of more than 25 years of CLEARSY’s experience in applying formal methods and designing safety critical systems.