Thèmes Participants Résumé Rapports Réunions Bibliographie Publications

CORTOS est une ACI "Sécurité Informatique". CORTOS signifie "Control and Observation of Real-Time Open Systems".

Thèmes abordés

• Synthèse de contrôleur
• Systèmes temps-réel
• Automates temporisés
• Vérification de systèmes ouverts
• Observation

Participants à l'ACI

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

Les noms en gras correspondent aux responsables de l'ACI dans les différents établissements partenaires.

Résumé du projet

La plupart des systèmes critiques actuels intègrent un module de contrôle/commande dont le bon fonctionnement est essentiel pour la sécurité de l'ensemble. C'est le cas notamment des systèmes embarqués, utilisés en avionique et en automatique industrielle. Un système dont l'évolution dépend de l'environnement dans lequel il est plongé est qualifié d'ouvert. La synthèse de contrôleur consiste, lorsque cela est possible, à construire un programme (le contrôleur) qui pilote les mécanismes d'interaction avec l'environnement de façon à garantir un fonctionnement sûr et correct, éventuellement dans un environnement hostile. Le système résultant de l'adjonction du contrôleur est alors fermé. Le contrôleur construit doit être contraignant pour garantir les propriétés de sécurité, mais doit être suffisamment permissif pour ne pas réduire inutilement les comportements du système. Les problèmes de contrôle ont été relativement bien étudiés pour les systèmes discrets non temporisés depuis deux décennies, et les questions théoriques majeures sont aujourd'hui résolues. Cependant, de nombreux systèmes intègrent une notion explicite de temps, par exemple en exigeant des délais de réponse. Grâce à l'introduction des automates temporisés et des automates hybrides au début des années 1990, la vérification de tels systèmes a connu un développement important, tant sur le plan théorique que pratique. Les jalons sont donc maintenant posés pour pouvoir attaquer le problème de la synthèse de contrôleur dans un cadre temporisé. Quelques travaux ont déjà vu le jour, mais les résultats obtenus sont disparates et ne tiennent pas suffisamment compte de la spécificité des systèmes temporisés. Par exemple, il est nécessaire d'intégrer des aspects temps-réel dans l'observation des systèmes ayant certains comportements masqués, de prendre en compte un temps non discret, et d'exprimer la correction du contrôle, ce qui est nettement plus difficile que d'énoncer les propriétés de sûreté classiques. Dans ce projet, nous envisageons de poursuivre l'étude du contrôle temporisé, les travaux existant à ce jour étant peu nombreux. Nous proposons d'aborder les points suivants :

• établir un cadre unifié permettant de comparer les modèles et les résultats existants ;
• utiliser une approche compositionnelle pour résoudre le problème de la synthèse de contrôleur ;
• étudier les liens entre la synthèse de contrôleur temporisé, l'observation de ces systèmes et la détection de fautes ;
• développer une bibliothèque de programmes pour la synthèse de contrôleurs s'intégrant aux outils existants dédiés à l'analyse des systèmes temporisés.

Rapports

• Rapport à mi-parcours (avril 2005)
• Rapport final (octobre 2006)

Réunions

• Première réunion : vendredi 31 octobre 2003 à Cachan
• Réunion des ACI SI les 11 et 12 décembre à Rennes
• Deuxième réunion : vendredi 5 mars 2004 à Grenoble
• Troisième réunion : lundi 7 et mardi 8 juin 2004 à Nantes
• Quatrième réunion : lundi 20 et mardi 21 septembre 2004 à Grenoble
• Réunion des ACI SI du 15 au 17 novembre 2004 à Toulouse
• Cinquième réunion : jeudi 3 et vendredi 4 février 2005 à Cachan
• Sixième réunion : lundi 6 et mardi 7 juin à Nantes
• Conférence MSR'05 : CORTOS y a une session invitée
  
  • Introduction au contrôle des systèmes temps-réel (transparents de l'exposé)
  • Observation partielle des systèmes temporisés (transparents de l'exposé)
  • Implémentabilité des automates temporisés (transparents de l'exposé)
• Réunion commune des ACI Cortos, Persée et Versydis : mardi 14 et mercredi 15 mars 2006 à Cachan
• Workshop CORTOS'06, associé à CONCUR'06 : le 31 août 2006 à Bonn (Allemagne)

Publications

• Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Optimal strategies in priced timed game automata. Research Report RS-04-4, Basic Research in Computer Science, Denmark, February 2004. 32 pages. Web page.
• Moez Krichen and Stavros Tripakis. Black-box conformance testing for real-time systems. In Proc. 11th International SPIN Workshop on Model-Checking of Software (SPIN'04), LNCS 2989, pp.109-126, Springer, 2004.
• Patricia Bouyer, Ed Brinksma and Kim G. Larsen. Staying alive as cheaply as possible. In Proc. 7th International Workshop on Hybrid Systems: Computation and Control (HSCC'04), LNCS 2993, pp.203-218, Springer, 2004.
• Olivier (H.) Roux and Didier Lime. Time (Petri) Nets with Inhibitor Hyperarcs. (Formal) Semantics ans State Space Computation. In Proc. 25th International Conference on Application and Theory of (Petri) Nets (ICATPN'04), LNCS 3099, pp. 371-390, Springer, 2004.
• Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Synthesis of optimal strategies using HyTech. In Proc. Workshop on Games in Design and Verification (GDV 2004), ENTCS 119(1), pp. 11-31. Elsevier, 2005.
• Franck Cassez and Olivier (H.) Roux. Structural Translation from Time (Petri) Nets to Timed Automata. In Proc. 4th International Workshop on Automated Verification of Critical Systems (AVoCS'04), ENTCS, Elsevier, 2004. To appear.
• Moez Krichen and Stavros Tripakis. Real-time testing with timed automata testers and coverage criteria. In Proc. Joint Conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant Systems (FORMATS+FTRTFT'2004), LNCS 3253, pp. 134-151. Springer, 2004
• Didier Lime and Olivier (H.) Roux. A Translation Based Method for the Timed Analysis of Scheduling Extended Time (Petri) Nets. In Proc. 25th IEEE International Real-Time Systems Symposium (RTSS'04), pp. 187-196. IEEE Computer Society Press, 2004.
• Patricia Bouyer, Franck Cassez, Emmanuel Fleury and Kim G. Larsen. Optimal strategies in priced timed game automata. In Proc. 24th Conference on Foundation of Software Technology and Theoretical Computer Science (FST&TCS 2004), LNCS 3328, pp. 148-160. Springer, 2004.
• Fabrice Chevalier. Détection d'erreurs dans les systèmes temporisés. Mémoire du DEA Algorithmique, 2004.
• Guillaume Gardey, Olivier (H.) Roux and Olivier (F.) Roux. State Space Computation and Analysis of Time (Petri) Nets. Journal Theory and Practice of Logic Programming (TPLP), Special Issue on Specification Analysis and Verification of Reactive Systems, 2005. To appear.
• Patricia Bouyer, Fabrice Chevalier and Deepak D'Souza. Fault Diagnosis using Timed Automata. In Proc. 8th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'05), LNCS 3441, pp.219-233, Springer, 2005.
• Karine Altisen, Florence Maraninchi, and David Stauch. Exploring aspects in the context of reactive systems. In Proc. Workshop Foundations of Aspect-Oriented Languages (FOAL'04), pages 45--51, 2004.
• Karine Altisen, Florence Maraninchi, and David Stauch. Aspect-oriented programming for reactive systems: a proposal in the synchronous framework, 2005. Submitted to Science of Computer Programming, (Special Issue on Foundations of Aspect-Oriented Programming).
• Patricia Bouyer, Ed Brinksma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in Systen Design, 2005. To appear.
• Patricia Bouyer, Franck Cassez, and François Laroussinie. Modal logics for timed control. Research Report RI-2005-3, IRCCyN/CNRS, Nantes, France, 2005.
• Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and François Vernadat. Reachability problems and abstract state spaces for time Petri nets with stopwatches. Technical Report 04483, LAAS, 2004.
• Thao Dang. Application of reachability analysis to idle speed control synthesis. International Journal of Software Engineering & Knowledge Engineering (IJSEKE), 2005. Special issue of selected papers from the International Embedded and Hybrid Systems Conference (IEHSC'05). To appear.
• Stavros Tripakis. Undecidable Problems in Decentralized Observation and Control for Regular Languages. In Information Processing Letters, vol. 90, issue 1, pp. 21-28, 2006
• Stavros Tripakis. Decentralized observation problems. CDC-ECC'05
• Stéphane Demri, Ranko Lazic, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. In Proc. 12th International Symposium on Temporal Representation and Reasoning (TIME'05). IEEE Computer Society Press, 2005. To appear.
• Philippe Gerner and Thao Dang. Computing schedules for multithreaded real-time programs using geometry. In Proc. Joint Conference on Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault Tolerant System (FORMATS+FTRTFT'04), LNCS 3253, pp. 325-342. Springer, 2004.
• Moez Krichen and Stavros Tripakis. An expressive and implementable formal framework for testing real-time systems. In Proc. 17th IFIP International Conference on Testing of Communicating Systems (TESTCOM'05), LNCS, Springer, 2005. To appear.
• Saddek Bensalem, Marius Bozga, Moez Krichen, Stavros Tripakis. Testing conformance of real-time applications by automatic generation of observers. In Proc. 4th International Workshop Runtime Verification (RV'04), ENTCS, Elsevier, 2004. To appear.
• Stavros Tripakis. Undecidable problems of decentralized observation and control on regular languages. Information Processing Letters (IPL), 90(1):21--28, 2004.
• Stavros Tripakis. Two-phase distributed observation problems. In Proc. 5th International Conference on Application of Concurrency to System Design (ACSD'05). IEEE Computer Society Press, 2005. To appear.
• Karine Altisen, Patricia Bouyer, Thierry Cachat, Franck Cassez, Guillaume Gardey. Introduction au contrôle des systèmes temps-réel. Journal Européen des Systèmes Automatisés, vol. 39, p. 367-380, 2005.
• Patricia Bouyer, Fabrice Chevalier, Moez Krichen, Stavros Tripakis. Observation partielle des systèmes temporisés. Journal Européen des Systèmes Automatisés, vol. 39, p. 381-393, 2005.
• Karine Altisen, Nicolas Markey, Pierre-Alain Reynier, Stavros Tripakis. Implémentabilité des automates temporisés. Journal Européen des Systèmes Automatisés, vol. 39, p. 395-406, 2005.
• Patricia Bouyer, Franck Cassez and François Laroussinie. Modal Logics for Timed Control. In Proc. 16th International Conference on Concurrency Theory (CONCUR'05), LNCS 3653, pp. 81-94. Springer, 2005
• Sophie Pinchinat and Stéphane Riedweg. You Can Always Compute Maximally Permissive Controllers Under Partial Observation When They Exist. In Proc.24th American Control Conference (ACC'05), pp. 2287-2292, 2005
• Stéphane Demri, David Nowak. Reasoning about transfinite sequences (extended abstract). In Proc. 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA'05), LNCS 3707, pp. 248-262. Springer, 2005
• Sophie Pinchinat and Stéphane Riedweg. On the Architectures in Decentralized Supervisory Control. In Proc. 44th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC'05), pp. 12-17. IEEE Computer Society Press, 2005.
• Patricia Bouyer, Thomas Brihaye and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters 98(5), pp. 188-194, 2006
• Patricia Bouyer and Fabrice Chevalier. On the Control of Timed and Hybrid Systems. EATCS Bulletin 89, pages 79-96, 2006
• Patricia Bouyer. Weighted Timed Automata: Model-Checking and Games. In Proc. 22nd Conference on Mathematical Foundations of Programming Semantics (MFPS'06), ENTCS 158, pp. 3-17. Elsevier Science Publishers, 2006
• Guillaume Gardey, Olivier (F.) Roux, and Olivier (H.) Roux. Safety control synthesis for time Petri nets. In Proc. 8th International Workshop on Discrete Event Systems (WODES'06), pp. 222-228. IEEE Computer Society Press, 2006 [ bib ]
• Karine Altisen, Franck Cassez and Stavros Tripakis. Monitoring and Fault Diagnosis with Digital Clocks. ACSD'06
• Patricia Bouyer, Thomas Brihaye and Fabrice Chevalier. Control in o-Minimal Hybrid Systems. In Proc. 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), pp. 367-378. IEEE Computer Society Press, 2006
• Patricia Bouyer, Laura Bozzelli and Fabrice Chevalier. Controller Synthesis for MTL Specifications. In Proc. 17th International Conference on Concurrency Theory (CONCUR'06), LNCS 4137, pp. 450-464. Springer, 2006
• François Laroussinie, Nicolas Markey and Ghassan Oreiby. Model Checking Timed ATL for Durational Concurrent Game Structures. In Proc. 4th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'06), LNCS 4202, pages 245-259. Springer, 2006
• Régis Gascon and Laura Bozzelli. Branching Time Temporal Logic Extended with Presburger Constraints. In Proc. 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'06), LNCS. Springer, 2006, to appear
• Thierry Cachat. Controller Synthesis & Ordinal Automata. In Proc. 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), Springer, 2006, to appear
• Patricia Bouyer, Kim G. Larsen, Nicolas Markey and Jacob I. Rasmussen. Almost Optimal Strategies in One-Clock Priced Timed Automata. In Proc. 26th Conference on Fundations of Software Technology and Theoretical Computer Science (FSTTCS'06), LNCS. Springer, 2006. To appear

---

Dernières modifications effectuées le 22 novembre 2006 par Patricia Bouyer.