Journal Article
Towards Cooperation of Formal Methods for the Analysis of Critical Control Systems
2011-10-18
2011-01-2558
Critical systems are subject to drastic certification constraints (DO178-B for avionic systems, SIL-4 for railway systems, ISO26262 for the automotive domain), which require system providers to produce strong evidence for the correctness, reliability, or performance of their systems. Today, the early use of formal modeling and verification methods is recognized as favorable by the industry. Formal methods, which started to appear in the 60's, have now reached a maturity level allowing them to be used in an industrial context. The approach of control system modeling as proposed by the MathWorks with MATLAB Simulink, by Esterel Technologies with the SCADE language or by the academic community with the Lustre language, is extensively used for reactive systems design and often allows the automatic generation of the embedded code.
