en
Systèmes Distribués, Ouverts, Temporisés ANR     SETIN




Thématiques de recherche

Participants

IRCCyN (Nantes) IRISA (Rennes) LaBRI (Bordeaux) LAMSADE (Paris) LSV (Cachan)
Gilles Benattar
Franck Cassez
Camille Constant
Didier Lime
Olivier H. Roux
Thomas Gazagnaire
Blaise Genest
Bartosz Grabiec
Loïc Hélouet
Claude Jard
Hugo Gimbert
Frédéric Herbreteau
Florian Horn*
David Janin
Anca Muscholl
Igor Walukiewicz
Pascal Weil
Marc Zeitoun
Béatrice Bérardo
Serge Haddad+
Benedikt Bollig
Patricia Bouyer
Romain Brenguier
Thomas Chatain
Dorsaf El Hog
Paul Gastin
François Laroussinie*
Nicolas Markey
Akshay Sundararaman
Michael Ummels
* Membres du LIAFA, Univ. Paris 7
+ Membre du LSV, ENS Cachan
o Membre du LIP6, Univ. Paris 6

Description du projet

Le projet DOTS porte sur la spécification formelle et la vérification automatique des systèmes informatiques. Plus particulièrement il s'intéresse aux systèmes complexes, comme les fameux systèmes embarqués, qui intègrent des aspects temporisés (des contraintes temps-réel), des aspects distribués (ces systèmes contiennent plusieurs composants qui communiquent entre eux) et des aspects interactifs avec leur environnement (on parle alors de systèmes ouverts). Si chacun de ces aspects pris séparément est aujourd'hui bien connu, la vérification de systèmes combinant plusieurs de ces caractéristiques reste un problème largement ouvert.

L'objectif du projet DOTS est de permettre des avancées théoriques et algorithmiques (validées par des prototypes) pour la conception de systèmes temporisés, distribués et ouverts. Une caractéristique essentielle du projet est de rassembler des spécialistes de chacun des trois aspects mentionnés ci-dessus pour confronter les techniques propres à chaque domaine et aborder conjointement la vérification des systèmes complexes.

Nous nous intéresserons principalement au model checking (est-ce qu'un système vérifie une propriété donnée ?), mais aussi au problème du contrôle (comment superviser un système pour qu'il vérifie une propriété de correction donnée ?) et au problème de la non-interférence (comment s'assurer qu'un système ne communique pas certaines informations sensibles à un observateur extérieur ?).

Pour attaquer ces problèmes, nous travaillerons autour de deux approches particulières. D'une part, nous utiliserons le cadre des jeux pour modéliser et analyser les interactions des systèmes. Et d'autre part, nous utiliserons les méthodes à base d'ordres partiels pour appréhender les aspects distribués. Combiner ces techniques en y intégrant aussi des contraintes temps-réel est une perspective novatrice et constitue une spécificité importante de notre projet.


Une présentation plus détaillée est donnée dans le texte complet du projet.

Rapports

— Rapports semestriels d'activité —

— Délivrables —

Réunions

Publications

2007 —

DT [ABG07] S. Akshay, Benedikt Bollig and Paul Gastin. Automata and Logics for Timed Message Sequence Charts. In FSTTCS'07, LNCS 4855, p. 290-302. Springer, 2007.
T [AMN07] S. Akshay, Madhavan Mukund, and K. Narayan Kumar. Checking Coverage for Infinite Collections of Timed Scenarios. In CONCUR'07, LNCS 4703, p. 181-196. Springer, 2007.
OT [BCD+07] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Uppaal-Tiga: Time for playing games!. In CAV'07, vol. 4590 of LNCS, p. 121-125. Springer, 2007.
D [BGMN07] Puneet Bhateja, Paul Gastin, Madhavan Mukund and K. Narayan Kumar. Local testing of message sequence charts is difficult. In FCT'07, vol. 4639 of LNCS, p. 76-87. Springer, 2007.
T [BGP07] Béatrice Bérard, Paul Gastin and Antoine Petit. Timed substitutions for regular signal-event languages. Formal Methods in System Design 31(2), pages 101-134, 2007.
T [BLM07] Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model-Checking One-Clock Priced Timed Automata. In FoSSaCS'07, vol. 4423 of LNCS, p. 108-122. Springer, 2007.
OT [BLMO07] Thomas Brihaye, François Laroussinie, Nicolas Markey and Ghassan Oreiby. Timed Concurrent Game Structures. In CONCUR'07, LNCS 4703, p. 445-459. Springer, 2007.
T [BM07] Patricia Bouyer and Nicolas Markey. Costs are Expensive!. In FORMATS'07, vol. 4763 of LNCS, p. 53-68. Springer, 2007.
T [BMOW07] Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James B. Worrell. The Cost of Punctuality. In LICS'07, p. 109-118. IEEE Comp. Soc. Press, 2007.
DT [BR07] Marc Boyer and Olivier H. Roux. Comparison of the expressiveness of Arc, Place and Transition Time Petri Nets. In ICATPN'07, vol. 4546 of LNCS, p. 63-82. Springer, 2007.
OT [Cas07] Franck Cassez. Efficient on-the-fly algorithms for partially observable timed games. In FORMATS'07, vol. 4763 of LNCS, p. 5-24. Springer, 2007.
OT [CDL+07] Franck Cassez, Alexandre David, Kim G. Larsen, Didier Lime, and Jean-François Raskin. Timed control with observation based and stuttering invariant strategies. In ATVA'07, LNCS 4762, p. 192-206. Springer, 2007.
DT [CMR07] Franck Cassez, John Mullins, and Olivier H. Roux. Synthesis of Non-Interferent Distributed Systems. In MMM-ACNS'07, CCIS 1, p. 307-321. Springer, 2007.
O [CTA07b] Franck Cassez, Stavros Tripakis, and Karine Altisen. Synthesis of optimal dynamic observers for fault diagnosis of discrete-event systems. In TASE'07, p. 316-325. IEEE Comp. Soc. Press, 2007.
D [EGP07] Edith Elkind, Blaise Genest, and Doron Peled. Detecting Races in Ensembles of Message Sequence Charts. In TACAS'07, vol. 4424 of LNCS, p. 420-434. Springer, 2007.
D [EGPS07] Edith Elkind, Blaise Genest, Doron Peled, and Paola Spoletini. Quantifying the Discord: Order Discrepancies in Message Sequence Charts. In ATVA'07, vol. 4762 of LNCS, p. 378-393. Springer, 2007.
D [GGH+07] Thomas Gazagnaire, Blaise Genest, Loïc Hélouët, P.S. Thiagarajan, and Shaofa Yang. Causal High Level Message Sequence Charts. In CONCUR'07, LNCS 4703, p. 166-180. Springer, 2007.
D [GK07] Paul Gastin and Dietrich Kuske. Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces. Fundamenta Informaticae 80(1-3), p. 169-197. IOS Press, 2007.
D [GKM07] Blaise Genest, Dietrich Kuske and Anca Muscholl. On communicating automata with bounded channels. Fundamenta Informaticae 80(1-3), p. 147-167. IOS Press, 2007.
D [HST07] Frédéric Herbreteau, Grégoire Sutre and The Quang Tran. Unfolding Concurrent Well-Structured Transition Systems. In TACAS'07, vol. 4424 of LNCS, p. 706-720. Springer, 2007.
D [MW07] Anca Muscholl and Igor Walukiewicz. A lower bound on Web services composition. In FoSSaCS'07, vol. 4423 of LNCS, p. 274-286. Springer, 2007.

2008 —

DT [ABG+08] S. Akshay, Benedikt Bollig, Paul Gastin, Madhavan Mukund and K. Narayan Kumar. Distributed Timed Automata with Independently Evolving Clocks. In CONCUR'08, vol. 5201 of LNCS, p.~nbsp;82-97. Springer, 2008.
T [BBB+08] Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Größer. Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata. In LICS'08, p. 217-226. IEEE Computer Society Press, 2008.
OT [BBJ+08] Patricia Bouyer, Thomas Brihaye, Marcin Jurdzinski, Ranko Lazic, and Michal Rutkowski. Average-Price and Reachability-Price Games on Hybrid Automata with Strong Resets. In FORMATS'08, vol. 5215 of LNCS, p. 63-77. Springer, 2008.
DT [BCH+08] Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier H. Roux. When are Timed Automata Weakly Timed Bisimilar to Time Petri Nets?. Theoretical Computer Science 403(2-3):202-220. Esleview, 2008.
DO [BCHK08] Paolo Baldan, Thomas Chatain, Stefan Haar, and Barbara König. Unfolding-based Diagnosis of Systems with an Evolving Topology. In CONCUR'08, vol. 5201 of LNCS, p. 203-217. Springer, 2008.
OT [BFL+08] Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey and Jiri Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In FORMATS'08, vol. 5215 of LNCS, p. 33-47. Springer, 2008.
O [BGMR08] Thomas Brihaye, Mohamed Ghannem, Nicolas Markey and Lionel Rieg. Good friends are hard to find!. In TIME'08, p. 32-40. IEEE Computer Society Press, 2008.
DT [BHR08] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. In Information and Computation, 206(1):73-107. Elsevier, 2008.
T [BLM08] Patricia Bouyer, Kim G. Larsen and Nicolas Markey. Model-Checking One-Clock Priced Timed Automata. Logical Methods in Computer Science 4(2:9), 2008.
T [BMOW08] Patricia Bouyer, Nicolas Markey, Joël Ouaknine and James B. Worrell. On Expressiveness and Complexity in Real-time Model Checking. In ICALP'08, vol. 5126 of LNCS, p. 124-135. Springer, 2008.
OT [BMR08] Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier. Robust Analysis of Timed Automata via Channel Machines. In FoSSaCS'08, vol. 4962 of LNCS, p. 157-171. Springer, 2008.
OT [DDMR08] Martin De Wulf, Laurent Doyen, Nicolas Markey and Jean-François Raskin. Robust Safety of Timed Automata. Formal Methods in System Design 33(1-3):45-84. Springer, 2008.
D [DGH08] Philippe Darondeau, Blaise Genest, and Loïc Hélouet. Products of Message Sequence Charts. In FOSSACS'08, vol. 4962 of LNCS, p. 459-474. Springer, 2008.
DO [DGTY08] Philippe Darondeau, Blaise Genest, P.S. Thiagarajan, and Shaofa Yang. Quasi-Static Scheduling of Communicating Tasks. In CONCUR'08, vol. 5201 of LNCS, p. 310-324. Springer, 2008.
D [GM08] Blaise Genest, Anca Muscholl. Pattern Matching and Membership for Hierarchical Message Sequence Charts. Theory of Computing Systems 42(4):536-567. Springer, 2008.

2009 —

OT [ACEF09] Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. An Inverse Method for Parametric Timed Automata. International Journal of Foundations of Computer Science 20(5):819-836, 2009.
OT [BCDL09] Peter Bulychev, Thomas Chatain, Alexandre David, and Kim G. Larsen. Checking simulation relation between timed game automata. In FORMATS'09, vol. 5813 of LNCS, p. 73-87. Springer, 2009.
O [BDLM09] Thomas Brihaye, Arnaud Da Costa, François Laroussinie, and Nicolas Markey. ATL with Strategy Contexts and Bounded Memory. In LFCS'09, vol. 5407 of LNCS, p. 92-106. Springer, 2009.
O [BDMR09] Patricia Bouyer, Marie Duflot, Nicolas Markey, and Gabriel Renault. Measuring Permissivity in Finite Games. In CONCUR'09, vol 5710 of LNCS, p. 196-210. Springer, 2009.
OT [BF09] Patricia Bouyer and Vojtech Forejt. Reachability in Stochastic Timed Games. In ICALP'09, vol 5556 of LNCS, p. 103-114. Springer, 2009.
DO [BGG09] Nathalie Bertrand, Blaise Genest and Hugo Gimbert. Qualitative Determinacy and Decidability of Stochastic Games with Signals. In LICS'09, p. 309-318, IEEE COmputer Society Press, 2009.
DO [BGH09] Benedikt Bollig, Manuela-Lidia Grindei, and Peter Habermehl. Realizability of Concurrent Recursive Programs. In FoSSaCS'09, vol. 5504 of LNCS, p. 410-424. Springer, 2009.
TD [BH09] Béatrice Bérard and Serge Haddad. Interrupt Timed Automata. In FoSSaCS'09, vol 5504 of LNCS, p. 410-424. Springer, 2009.
T [BHR09] Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Undecidability Results for Timed Automata with Silent Transitions. Fundamenta Informaticae 92(1-2):1-25. IOS Press, 2009.
D [BRBH09] Anne Bouillard, Sidney Rosario, Albert Benveniste, and Stefan Haar. Monotonicity in Service Orchestrations. In ICATPN'09, vol. 5606 of LNCS, p. 263-282. Springer, 2009.
OT [CDL09] Thomas Chatain, Alexandre David, and Kim G. Larsen. Playing Games with Timed Games. In ADHS'09, 2009.
DO [CGS09] Thomas Chatain, Paul Gastin, and Nathalie Sznajder. Natural Specifications Yield Decidability for Distributed Synthesis of Asynchronous Systems. In SOFSEM'09, vol. 5404 of LNCS, p. 141-152. Springer, 2009.
OT [CM09] Franck Cassez and Nicolas Markey. Control of Timed Systems. In Communicating Embedded Systems - Software and Design, chap. 3. Wiley-ISTE, 2009.
D [DG09] Volker Diekert and Paul Gastin. Local safety and local liveness for distributed systems. In Perspectives in Concurrency Theory, p. 86-106. Universities Press, 2009.
O [GH09] Hugo Gimbert and Florian Horn. Solving Simple Stochastic Games with Few Random Vertices. Logical Methods in Computer Science 5(2), 2009.
DT [GMN09] Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Reachability and boundedness in time-constrained MSC graphs. In Perspectives in Concurrency Theory, p. 157-183. Universities Press, 2009.
DO [GSZ09] Paul Gastin, Nathalie Sznajder, and Marc Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design 34(3):215-237. Springer, 2009.
OT [JR09] Claude Jard and Olivier H. Roux (eds). Communicating Embedded Systems – Software and design. Wiley-ISTE, 2009.
DT [RS09] Pierre-Alain Reynier and Arnaud Sangnier. Weak Time Petri Nets strike back!. In CONCUR'09, vol. 5710 of LNCS, pages 557-571. Springer, 2009.

2010 —

DO [BCHK10] Paolo Baldan, Thomas Chatain, Stefan Haar, and Barbara König. Unfolding-based Diagnosis of Systems with an Evolving Topology. Information and Computation. Elsevier, 2010. To appear.
OT [BCL10] Patricia Bouyer, Franck Cassez, and François Laroussinie. Timed Modal Logics for Real-Time Systems: Specification, Verification and Control. Journal of Logic, Language and Information, 2010. To appear.
T [BCM10] Patricia Bouyer, Fabrice Chevalier, and Nicolas Markey. On the Expressiveness of TPTL and MTL. Information and Computation 208(2):97-116. Elsevier, 2010.
D [BEGP09] Dragan Bosnacki, Edith Elkind, Blaise Genest, and Doron Peled. On Commutativity Based Edge Lean Search. Annals Math & AI 56(2):187-210. Springer, 2009.
T [BFLM10] Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, and Nicolas Markey. Timed Automata with Observers under Energy Constraints. In HSCC'10. ACM Press, 2010. To appear.
DO [BH10] Benedikt Bollig and Loïc Hélouët. Realizability of Dynamic MSC Languages. In CSR'10, LNCS. Springer, 2010. To appear.
DO [CF10] Thomas Chatain and Éric Fabre. Factorization Properties of Symbolic Unfoldings of Colored Petri Nets. In ICATPN'10, LNCS. Springer, 2010. To appear.
DT [CJ10] Thomas Chatain and Claude Jard. Sémantique concurrente symbolique des réseaux de Petri saufs et dépliages finis des réseaux temporels. In NOTERE'10. IEEE Computer Society Press, 2010. To appear.
DO [DGTY10] Philippe Darondeau, Blaise Genest, P.S. Thiagarajan, and Shaofa Yang. Quasi-Static Scheduling of Communicating Tasks. Information and Computation. Elsevier, 2010. To appear.
D [EGPS10] Edith Elkind, Blaise Genest, Doron Peled, and Paola Spoletini. Quantifying the Discord: Order Discrepancies in Message Sequence Charts. International Journal of Foundations of Computer Science 21(2):211-233. WorldSciNet, 2010.
D [GGHTY09] Thomas Gazagnaire, Blaise Genest, Loïc Hélouet, P.S. Thiagarajan, and Shaofa Yang. Causal Message Sequence Charts. Theoretical Computer Science 410(41): 4094-4110, Elsevier, 2009.
DO [GGMW10] Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Optimal Zielonka-Type Construction of Deterministic Asynchronous Automata. In ICALP'10, LNCS. Springer, 2010. To appear.
O [GH10] Hugo Gimbert and Florian Horn. Solving Simple Stochastic Tail Games. In SODA'10, p. 847-862. SIAM, 2010.
D [GK10] Paul Gastin and Dietrich Kuske. Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces. Information and Computation. Elsevier, 2010. To appear.
D [HLMS10] Alexander Heussner, Jerome Leroux, Anca Muscholl, and Gregoire Sutre. Reachability Analysis of Communicating Networks with Pushdowns. In FOSSACS'10, vol. 6014 of LNCS. Springer, 2010.
T [HSW10] Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Efficient Emptyness Check for Timed Büchi Automata. In CAV'10, LNCS. Springer, 2010.




Page maintenue par Nicolas Markey.
Dernières modifications : 9 février 2012.
Valid HTML 4.01! Valid CSS!