Modeling and Information Processing
Engineering of critical systems
Activities and applications
Activities
The activities are firstly formal verification activities. They mainly consist of modeling, expressing the properties of, selecting and applying the suitable verification techniques. They concern the methods and their integration in the development process. They also concern and are involved in the development of certification standards.
The activities also seek to perform a formal assessment to guide design choices. In this case, it may be a question of finding a solution that meets some criteria. It may also be a question of optimizing and finding the best solution.
Lastly, the activities also cover the languages, techniques and formal tools. Thus, they mainly involve adapting and developing techniques and tools or adapting and defining the modeling languages.
Example of applications
Formal assessment of properties is very useful for developing aeronautic systems.
Regarding an aircraft hydraulic generation system, it is used to ensure that, for example, in all scenarios "if we have less than 2 breakdowns, then there is no total loss of hydraulics". In this case it is a safety (RAMS) property.
Similarly, in case of avionic architecture, it is used to ensure that "the latency of a message from point x to point y is less than duration d". In this case it is a Real Time Performance (PTR) property.
Lastly, in flight control software, it can be used to ensure that "the spoilers are never deployed in flight". In this case it is a Functional Property (FXL) of the system.
There are other fields of application for these formal techniques: Space, Defense, Transport (automobile, rail), Telecom, smart cards, etc.
