MOSES team

Modèles et Outils formels pour des Systèmes à Evénements discrets Sûrs

Leader: Abdoul Toguyeni



The main scientific challenge of the MOSES team is to develop formal methods for the design and exploitation of dependable Discrete Event Systems (DES). Formal modeling forms the basis of the methods that we want to develop. Based on formalisms such as Petri Nets or Automata, we construct formal models of considered systems depending on the design or exploitation stages’ goals. We want to use techniques such as the transformation of models in order to move from formal models to others depending on the control and monitoring objectives. For example, model transformation can help to move from control models to diagnostic models. Similarly, to reduce design costs and to propose suitable methods for the design of critical systems, we want to integrate formal verification very early in the design process. Formal models also constitute an interesting tool for completing the design process and generate testing scenarios at each test step such as unitary or integration tests. To achieve these safety objectives, techniques such as model-checking or theorem proving can be used. Another objective is to involve on-the-shelf components to reduce the costs to design and to make new systems. The main obstacles we have to face are the combinatorial explosion and their safety. The use of formalisms with a high level of expressiveness (Timed automata, Time Petri Nets, …) and the use of modular or distributed techniques are methods we develop to offer solutions that are scalable. At the level application, we want to transfer our experience in the field of manufacturing systems, to the design of critical embedded systems. We will more particularly consider them for the control of rail transport systems. Part of our strategy is linked to our active participation, to the IRT RAILENIUM. In particular, our team is concerned with the design of the control and signaling for the next generation of trains. To deal with this objective, we are developing a railway benchmark UNIRAIL. It is an open test platform that will enable the testing of different systems for railway control and signaling. UNIRAIL complies with the European Railway Traffic Management System (ERTMS) and will permit the development of automatic train operation.




Paul Cazenave

Synthèse de contrôleurs pour la commande automatique des systèmes ferroviaires

Les autres équipes du groupe thématique ' CI2S '