The scientific context of the DOTS project is specification, verification and design of information systems. The research domain we have in mind started about 25 years ago with seminal papers by Clarke, Pnueli and Sifakis. Since then the domain has witnessed an impressive growth: a comprehensive theory has been developed, efficient algorithms have been designed, and tools like model checkers have been developed. These tools allow to verify automatically that a model of a system satisfies its specification. The research results have also penetrated the industry world as model checkers are now used in an industrial context for numerous case studies which in turn provided some feedback to improve the theory and algorithms.

Complex systems, such as embedded systems that are widely used nowadays (telecommunication, transport, automation), are often distributed —composed of several components that communicate together—, timed —contain timing constraints—, and open —interact with their environment. Each of these aspects considered separately is now relatively well understood and corresponds to an active research area. The big challenge is to deal with systems which present several of these features.

The aim of the DOTS project is to associate researchers specialized in verification of different aspects mentioned above in order to tackle problems that emerge when considering several features simultaneously. In this way we plan to significantly advance both theory as well as algorithmics of design and verification of distributed, open and timed systems.

The area of formal verification covers now a wide range of problems that share a common theoretical basis, but require specific approaches and techniques. In addition to model checking —the classical problem that consists in deciding whether a given model satisfies a given specification— the DOTS project will mainly address two important verification problems: control and non-interference.

An important characteristic of the DOTS project is our choice of methods and tools to address the problems mentioned above. We plan to use games to cope with interactive aspects and partial orders to deal with the distributed aspect.

More details are available in the full text of the proposal.

Reports

— Biannual activity report —

August 2007: coordinator.
March 2008: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.
September 2008: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.
March 2009: coordinator – LSV – LaBRI – IRISA – IRCCyN – LAMSADE.

— Deliverables —

Web site. April 2007.

D1.1: Quantitative objectives in timed games. September 2008.
D1.2a: Synthesis of timed controllers. March 2009.
D1.3a: Specification of Timed Non-Interference. March 2008.
D2.1: Theory of distributed games. September 2008.
D2.2: Distributed control for restricted specifications. March 2009.
D2.4b: Quantitative specifications for non-interference. January 2010.
D3.1a: Model for distributed timed systems. September 2008.
D4.1 Specification of realistic DOTS examples. September 2008.

Meetings

Kick-off meeting (Cachan, 12 February 2007).
Meeting on "unfolding of networks of timed automata" (Rennes, 4 April 2007).
Meeting on "Non-interference" (Nantes, 22 May 2007).
Meeting on "Timed games" (Cachan, 18 June 2007).
~~Meeting "DOTS-AVERISS" (Bordeaux, 15-16 November 2007).~~
Meeting on "unfolding" (Rennes, 10 January 2008).
Meeting "AVERISS-DOTS" (Bordeaux, 30-31 January 2008).
Meeting on "Non-interference" (Paris, 15 April 2008).
Meeting on "WP2" (Bordeaux, 15 April 2008).
~~Meeting on "Non-interference" (Nantes, 29 April 2008).~~
Meeting on "Non-interference" (Nantes, 5 June 2008).
Meeting on "unfolding" (Rennes, 3 December 2008).
DOTS meeting (Cachan, 20 January 2009).
Meeting on "Non-interference" (Montréal, 2-6 February 2009).
Meeting on "Non-interference" (Paris, 4 June 2009).
Meeting on case study (Rennes, 3 July 2009).
Meeting on WP2 (Bordeaux, 28-29 October 2009).
DOTS meeting (Nantes, 19 November 2009).
Meeting on "Non-interefernce" (Paris, 7 January 2010).
DOTS meeting (Bordeaux, 18 March 2010).

Publications

— 2007 —
	[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.
	[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.
	[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.
	[BEGP07]	Dragan Bosnacki, Edith Elkind, Blaise Genest, and Doron Peled. On Commutativity Based Edge Lean Search. In ICALP'07, vol. 4596 of LNCS, p. 158-170. Springer, 2007.
	[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.
	[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.
	[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.
	[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.
	[BM07]	Patricia Bouyer and Nicolas Markey. Costs are Expensive!. In FORMATS'07, vol. 4763 of LNCS, p. 53-68. Springer, 2007.
	[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.
	[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.
	[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.
	[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.
	[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.
	[CTA07a]	Franck Cassez, Stavros Tripakis, and Karine Altisen. Sensor minimization problems with static or dynamic observers for fault diagnosis. In ACSD'07, p. 90-99. IEEE Comp. Soc. Press, 2007.
	[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.
	[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.
	[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.
	[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.
	[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.
	[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.
	[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.
	[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 —
	[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.
	[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.
	[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.
	[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), pages 202-220, 2008.
	[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.
	[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.
	[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.
	[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.
	[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.
	[CDL08]	Thomas Chatain, Alexandre David, and K.im G. Larsen. Playing Games with Timed Games. Research Report LSV-08-34, Laboratoire Spécification et Vérification, ENS Cachan, France, 2008.
	[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.
	[DG08]	Volker Diekert and Paul Gastin. Local safety and local liveness for distributed systems. In Perspectives in Concurrency Theory. Universities Press, 2008.
	[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.
	[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.
	[GM08]	Blaise Genest, Anca Muscholl. Pattern Matching and Membership for Hierarchical Message Sequence Charts. Theory of Computing Systems 42(4):536-567. Springer, 2008.
	[GMSZ08]	Blaise Genest, Anca Muscholl, Olivier Serre, and Marc Zeitoun. Tree Pattern Rewrite Systems. In ATVA'08, vol. 5311 of LNCS, p. 332-346. Springer, 2008.
— 2009 —
	[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.
	[BH09]	Béatrice Bérard and Serge Haddad. Interrupt Timed Automata. In FoSSaCS'09, LNCS. Springer, 2009. To appear.
	[BHR09]	Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Undecidability Results for Timed Automata with Silent Transitions. In Fundamenta Informaticae, 2009. To appear.
	[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.
	[GMN09]	Paul Gastin, Madhavan Mukund, and K. Narayan Kumar. Reachability and boundedness in time-constrained MSC graphs. In Perspectives in Concurrency Theory, pages 157-183. Universities Press, 2009.
	[GSZ09]	Paul Gastin, Nathalie Sznajder, and Marc Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design, 2009. To appear.