Modeling and Information Processing
The engineering of critical systems
Design and formal evaluation of critical systems
Objectives
The objective is to develop formal means for controlling the design and validation of critical systems, using methods adapted to each level of development and each objective, to construct an optimized formal global vision of the systems, and making the link with the practice of industry in the area of verification (integration in the process, certification).
Areas of application
The areas of application are mainly embedded systems for transport at different levels of granularity (from software to aircraft systems).
Context
Critical systems require that their correct behaviour is ensured, and this is crucial. It is therefore necessary to be able to demonstrate the correctness of these systems in particular wrt the certification authorities.
The increase in the size and complexity of these systems makes the operations of verification and validation long and costly, even impossible to execute with conventional means such as simulation and testing.
Furthermore, multi-faceted development is characteristic of the development of these systems for which different aspects of the same system are studied by different teams: Functional (FXL), Real Time Performance (RTP) and RAMS (Reliability, Availability, Maintainability, Safety) may all constitute a facet of the same system.
Formal methods
These methods make use of techniques based on mathematics for the specification, development and the verification of systems. They are used in particular for the automatic computation of system properties. This computation of properties provides the basis for a demonstration of the correctness of a system. Their value resides essentially in the exhaustive and automatic character of the proofs provided. They offer a wide range of languages and techniques for the different facets and verification objectives.
