Published: 26th October 2014 DOI: 10.4204/EPTCS.166 ISSN: 2075-2180 |
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 [1] that allow component specifications to be expressed as single TIOA or as assume-guarantee pairs.
The theory is implemented in the ECDAR tool [7], using the UPPAAL-TIGA [2] engine for timed games. The tool has – among others – been used for compositional, assume-guarantee based, verification of distributed scheduling protocols [7] and leader election protocols [6]. Comparing the execution times between compositional verification and classical “monolithic” verification shows in all cases a huge difference in favor of compositional verification.
[1] 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.
[2] 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.
[3] 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.
[4] 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.
[5] 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.
[6] 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.
[7] 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.