Published: 26th October 2014|
|Invited Presentation: Program Synthesis for Network Updates Pavol Černý||1|
|Invited Presentation: Playing Games with Timed Automata Kim G. Larsen||2|
|Concurrency Models with Causality and Events as Psi-calculi Håkon Normann, Cristian Prisacariu and Thomas Hildebrandt||4|
|An Intensional Concurrent Faithful Encoding of Turing Machines Thomas Given-Wilson||21|
|Toward Sequentializing Overparallelized Protocol Code Sung-Shik T.Q. Jongmans and Farhad Arbab||38|
|On-the-fly Probabilistic Model Checking Diego Latella, Michele Loreti and Mieke Massink||45|
|The Boolean Algebra of Cubical Areas as a Tensor Product in the Category of Semilattices with Zero Nicolas Ninin and Emmanuel Haucourt||60|
|From Orchestration to Choreography through Contract Automata Davide Basile, Pierpaolo Degano, Gian-Luigi Ferrari and Emilio Tuosto||67|
|A note on two notions of compliance Massimo Bartoletti, Tiziana Cimoli and G. Michele Pinna||86|
|Loosening the notions of compliance and sub-behaviour in client/server systems Franco Barbanera and Ugo de' Liguoro||94|
We first give a brief overview of program synthesis. We describe the role that declarative, logical specifications can play in making programmers more efficient. Second, we describe an application of this approach: synthesis of programs that update network configurations. Configuration updates are a leading cause of instability in networks. A key factor that makes updates difficult to implement is that networks are distributed systems with hundreds or thousands of nodes all interacting with each other. Even if the initial and final configurations are correct, naively updating individual nodes can easily cause the network to exhibit incorrect behaviors such as forwarding loops, black holes, and security vulnerabilities. This talk presents a new approach to the network update problem: we automatically generate updates that are guaranteed to preserve important correctness properties, given in a temporal logic. Our system is based on counterexample-guided search and incorporates heuristics that quickly identify correct updates in many situations. We exploit the fact that the search algorithm asks a series of related model checking questions, and develop an efficient incremental LTL model checking algorithm. We present experimental results showing that the tool efficiently generates updates for real-world network topologies with thousands of nodes.
A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design.
Using Timed I/O Automata a complete specification theory for real-time systems has been put forward in [4, 5, 3], with semantics given in terms of Timed I/O Transition Systems. In particular, the specification formalism comes equipped with constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications, all indispensable ingredients of a compositional design methodology. In fact, the specification theory has all the necessary constructs  that allow component specifications to be expressed as single TIOA or as assume-guarantee pairs.
The theory is implemented in the ECDAR tool , using the UPPAAL-TIGA  engine for timed games. The tool has – among others – been used for compositional, assume-guarantee based, verification of distributed scheduling protocols  and leader election protocols . Comparing the execution times between compositional verification and classical “monolithic” verification shows in all cases a huge difference in favor of compositional verification.
 Sebastian S. Bauer, Alexandre David, Rolf Hennicker, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman & Andrzej Wasowski (2012): Moving from Specifications to Contracts in Component-Based Design. In Juan de Lara & Andrea Zisman, editors: Fundamental Approaches to Software Engineering - 15th International Conference, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings, Lecture Notes in Computer Science 7212, Springer, pp. 43–58, doi: http://dx.doi.org/10.1007/978-3-642-28872-2_3.
 Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen & Didier Lime (2007): UPPAAL-Tiga: Time for Playing Games! In Werner Damm & Holger Hermanns, editors: Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, Lecture Notes in Computer Science 4590, Springer, pp. 121–125, doi: http://dx.doi.org/10.1007/978-3-540-73368-3_14.
 Timothy Bourke, Alexandre David, Kim G. Larsen, Axel Legay, Didier Lime, Ulrik Nyman & Andrzej Wasowski (2010): New Results on Timed Specifications. In Till Mossakowski & Hans-Jörg Kreowski, editors: Recent Trends in Algebraic Development Techniques - 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers, Lecture Notes in Computer Science 7137, Springer, pp. 175–192, doi: http://dx.doi.org/10.1007/978-3-642-28412-0_12.
 Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman & Andrzej Wasowski (2009): Methodologies for Specification of Real-Time Systems Using Timed I/O Automata. In Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede & Michael Leuschel, editors: Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers, Lecture Notes in Computer Science 6286, Springer, pp. 290–310, doi: http://dx.doi.org/10.1007/978-3-642-17071-3_15.
 Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman & Andrzej Wasowski (2010): Timed I/O automata: a complete specification theory for real-time systems. In Karl Henrik Johansson & Wang Yi, editors: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, 2010, ACM, pp. 91–100, doi: http://doi.acm.org/10.1145/1755952.1755967.
 Alexandre David, Kim Guldstrand Larsen, Axel Legay, Mikael H. Møller, Ulrik Nyman, Anders P. Ravn, Arne Skou & Andrzej Wasowski (2012): Compositional verification of real-time systems using Ecdar. STTT 14(6), pp. 703–720, doi: http://dx.doi.org/10.1007/s10009-012-0237-y.
 Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman & Andrzej Wasowski (2010): ECDAR: An Environment for Compositional Design and Analysis of Real Time Systems. In Ahmed Bouajjani & Wei-Ngan Chin, editors: Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings, Lecture Notes in Computer Science 6252, Springer, pp. 365–370, doi: http://dx.doi.org/10.1007/978-3-642-15643-4_29.