cortos3.gif CORTOS is a so-called "ACI" ("Action Concertée Incitative") in "Security" which is sponsored by the French Ministry of Research.
CORTOS means "Control and Observation of Real-Time Open Systems".

Research Themes


IRCCyN (Nantes) LSV (Cachan) VERIMAG (Grenoble)
Franck Cassez
Julien D'Orso
Guillaume Gardey
Didier Lime
Olivier Roux
Olivier-Henri Roux
Houda Bel Mokadem
Béatrice Bérard
Patricia Bouyer
Laura Bozzelli
Thierry Cachat
Fabrice Chevalier
Stéphane Demri
François Laroussinie
Nicolas Markey
Ghassan Oreiby
Antoine Petit
Pierre-Alain Reynier
Karine Altisen
Thao Dang
Moez Krichen
Stavros Tripakis

Names in bold shape correspond to the people who are responsible of this project in each unit.


Context of the project. Our project addresses the controller synthesis problem for real-time open systems. Most of the safety critical systems nowadays include a control program to supervise a plant. Such systems are often called embedded systems (e.g. nuclear plant, transport software, communication protocols, etc). They are critical in the sense that error can lead to the loss of lives or a major loss of money. This is why a great deal of research has been devoted to the formal verification of such systems. Among other techniques, model-checking consists in verifying that a model (of the plant and the control program running concurrently) meets some specification. It is now widely used in an industrial context and has turned out very successful in the design of critical systems. However, model-checking requires that the whole system is designed and the control program is given a priori.

A more difficult task consists in building a control program that supervises the plant in order to meet some requirements. In the automatic control community this problem has been extensively studied since the seminal work of Ramadge and Wonham about the supervisory control of discrete systems. How to build a controller for finite discrete event systems and when it can be done, are now well understood questions. This is not yet the case for timed systems, which involve real-time constraints. During the last decade, the model of timed automata (Alur and Dill) made it possible to reason about quantitative time. Model-checking was lifted to timed automata and is now supported by various tools (KRONOS, UPPAAL, CMC), which have been applied successfully to the verification of many industrial cases. The control synthesis problem for timed systems is of course more difficult, particularly because of the dense nature of time. It has been studied quite a lot recently but only partial results exist and there is no unified theory for the control of timed systems.

Core of the project. If we try to summarize the results about control synthesis for timed systems we find the following features: In this project, our main objectives are to increase the knowledge about control problems for timed systems and provide new methods for controller synthesis.




Last modifications, the 22nd november 2006 by Patricia Bouyer.
Valid HTML 4.01! Valid CSS!