Published: 26th October 2014
DOI: 10.4204/EPTCS.166
ISSN: 2075-2180

EPTCS 166

Proceedings 7th
Interaction and Concurrency Experience
Berlin, Germany, 6th June 2014

Edited by: Ivan Lanese, Alberto Lluch Lafuente, Ana Sokolova and Hugo Torres Vieira
Preface
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

Preface

This volume contains the proceedings of ICE'14, the 7th Interaction and Concurrency Experience, which was held in Berlin, Germany on the 6th of June 2014 as a satellite event of DisCoTec'14. The ICE workshop series has a main distinguishing aspect: the workshop features a particular review and selection procedure.
The previous editions of ICE were affiliated to ICALP'08 (Reykjavik, Iceland), CONCUR'09 (Bologna, Italy), DisCoTec'10 (Amsterdam, The Netherlands), DisCoTec'11 (Reykjavik, Iceland), DisCoTec'12 (Stockholm, Sweden) and DisCoTec'13 (Florence, Italy).
The ICE procedure for paper selection allows PC members to interact, anonymously, with authors. During the review phase, each submitted paper is published on a forum and associated with a discussion forum whose access is restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions that the authors reply to. As at the past six editions, the forum discussion during the review and selection phase of ICE'14 has considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for a lively discussion during the workshop. The interactive selection procedure implies additional effort for both authors and PC members. The effort and time spent in the forum interaction is rewarding for both authors -- when updating their papers -- and reviewers -- when writing their reviews: the forum discussion helps to discover and correct typos in key definitions and mispelled statements, to improve examples and presentation of critical cases, and solve any misunderstanding at the very early stage of the review process. Each paper was reviewed by three PC members, and altogether 8 papers were accepted for publication. We were proud to host two invited talks by Kim Larsen and Pavol Cerny, whose abstracts are included in this volume together with the regular papers. Final versions of the contributions, taking into account the discussion at the workshop, are included in the same order as they were presented at the workshop.
We would like to thank the authors of all the submitted papers for their interest in the workshop and the PC members for their efforts, which provided for the success of the ICE workshop. We thank Kim Larsen and Pavol Cerny for accepting our invitations to present their recent work, and the DisCoTec'14 organisers, in particular the general and workshop chairs, for providing an excellent environment for the preparation and staging of the event. Finally, we thank EPTCS editors for the publication of post-proceedings and the sponsors of the event, namely we acknowledge support by FCT through funding of LaSIGE Strategic Project, ref. PEst-OE/EEI/UI0408/2014.

FCT LASIGE


Ivan Lanese -- Focus Team, University of Bologna/INRIA (Italy)
Alberto Lluch Lafuente -- DTU Compute, Technical University of Denmark (Denmark)
Ana Sokolova -- University of Salzburg (Austria)
Hugo Torres Vieira -- LaSIGE, University of Lisbon (Portugal)

Program Synthesis for Network Updates

Pavol Černý (University of Colorado Boulder)

Abstract

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.

Playing Games with Timed Automata

Kim G. Larsen (Aalborg University)

Abstract

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.

References

[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.