Modeling and Information Processing
Engineering of critical systems
Research axes
There are three research axes on the theme of critical system engineering:
- Model driven engineering (MDE)
- Formal assessments
- Scalability of design and verification
Engineering of models
The research firstly relates to the expression of models by defining domain specific languages (DSL) through meta-modeling and by studying the semantics of modelling languages and associated tools. It also relates to procedures that can be used to plan consistent management of different modelling levels especially by using the following techniques:
- abstraction, based on a specific viewpoint to produce reduced models;
- refinement by enrichement of a model
The research on MDE also delves into modelling by aspects to include different viewpoints (secure operations, performance, costs, etc.). Hybrid models of continuous and discrete representations are studied, in particular.
This first axis also includes the study of model development techniques, development of simulation techniques allowing these models to be stimulated.
Formal assessments
The research projects into formal assessments aims to define specialized evaluations for a range of given requirements, by developing new techniques for given requirements or by including new types of requirements.
The research also covers the techniques used for making assessments that combine several families of requirements.
Lastly, it covers methods and techniques used to combine different formal assessments. The complementary natures of different verification techniques have to be studied in order to optimize the effectiveness of the overall verification. It also studies the links that can be made between evaluation techniques and techniques for guiding architecture design. Finally, it deals with the problems of integrating techniques of formal assessment of requirements concerning computing systems within the multi-disciplinary optimization methods and tools for designing aircraft.
Upgradeability
The research aims to develop approaches for upgradeable design and verification.
These approaches can be based on the definition of a pre-validated component concept and on the exploration of modular verification approaches specific to a given format (proof of programs, SCADE model checking, etc.). Techniques based on Design patterns or on composition of pre-validated bricks arise out of these approaches.
In this context, modular verification techniques that are independent of formal verification techniques used for each brick (generic assume-guarantee) are also of interest, which are thus used to get an abstraction in relation to the component or the property.
In general, the research also concerns managing upgrades especially by using techniques dedicated to reuse and incrementality. One objective could be to find ways of offering configured extension procedures for groups of systems.
