Published: 14th December 2012
DOI: 10.4204/EPTCS.104
ISSN: 2075-2180

EPTCS 104

Proceedings Fifth
Interaction and Concurrency Experience
Stockholm, Sweden, 16th June 2012

Edited by: Marco Carbone, Ivan Lanese, Alexandra Silva and Ana Sokolova
Preface
Invited Presentation: Conformance Testing of Interacting Components
Marcello Bonsangue		1
Reducing Weak to Strong Bisimilarity in CCP
Andrés Aristizábal, Filippo Bonchi, Luis Pino and Frank Valencia		2
Shared Contract-Obedient Endpoints
Étienne Lozes and Jules Villard		17
Metric-Aware Secure Service Orchestration
Gabriele Costa, Fabio Martinelli and Artsiom Yautsiukhin		32
Invited Presentation: Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications
Ichiro Hasuo		47
Towards a Theory of Glue
Simon Bliudze		48
Enforcing Architectural Styles in Presence of Unexpected Distributed Reconfigurations
Kyriakos Poyias and Emilio Tuosto		67
Coherent Minimisation: Towards efficient tamper-proof compilation
Dan R. Ghica and Zaid Al-Zobaidi		83
Interacting via the Heap in the Presence of Recursion
Jurriaan Rot, Irina Măriuca Asăvoae, Frank de Boer, Marcello M. Bonsangue and Dorel Lucanu		99

Preface

This volume contains the proceedings of ICE'12, the 5th Interaction and Concurrency Experience workshop, which was held in Stockholm, Sweden on the 16th of June 2012 as a satellite event of DisCoTec'12. The ICE workshop series has two distinguishing aspects: firstly, the workshop features a novel review and selection procedure and, secondly, each year, it focuses on a specific topic.
The previous editions of ICE were affiliated to ICALP'08 (Reykjavik, Iceland), CONCUR'09 (Bologna, Italy), DisCoTec'10 (Amsterdam, The Netherlands) and DisCoTec'11 (Reykjavik, Iceland) with focus on Synchronous and Asynchronous Interactions, on Structured Interactions, on Guaranteed Interactions, and on Reliable and Contract-based Interaction, respectively. The topic of ICE'12 was Distributed Coordination, Execution Models, and Resilient Interaction.
The ICE procedure for paper selection allows for 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 interests. The PC members post comments and questions that the authors reply to. As at the past three editions, the forum discussion during the review and selection phase of ICE'12 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 Marcello Bonsangue and Ichiro Hasuo, 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 Marcello Bonsangue and Ichiro Hasuo for accepting our invitations to present their recent work, and the DisCoTec'12 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 CEA LIST and the University of Bologna.

Marco Carbone -- ITU (Denmark)
Ivan Lanese -- University of Bologna/INRIA (Italy)
Alexandra Silva -- Radboud University Nijmegen (The Netherlands)
Ana Sokolova -- University of Salzburg (Austria)

Conformance Testing of Interacting Components

Marcello Bonsangue (LIACS & CWI, The Netherlands)


In component based software engineering, distributed components interact using complex coordination patterns that may be implemented by networks of communication channels. Channels receive stimuli from the environment possibly causing interactions to take place. In this talk I will introduce an execution model for channel based coordination, and present some principles and methods for testing implementations of coordination patterns to ensure their correct responses with respect to stimuli specifications.

Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications

Ichiro Hasuo (University of Tokyo, Japan)


*Hybrid systems* are those which exhibit both discrete "jump" and continuous "flow" dynamics. Their importance---as components of *cyber-physical systems*---is paramount now that more and more physical systems (cars, airplanes, etc.) are controlled with computers.

There are naturally two directions towards the study of hybrid systems: *control theory* (typically continuous) and *formal verification* (typically discrete). For us from the formal verification community, therefore, the big challenge is how to incorporate continuous "flow" dynamics. Many existing techniques---such as hybrid automaton or Platzer’s differential dynamic logic---include differential equations explicitly. This incurs a difficult (and very interesting) question of how to handle differential equations.

In our project we take a different path of *turning flow into jump*---more precisely into infinitely many jumps each of which is infinitesimal (i.e. infinitely small). This makes everything discrete jump dynamics, to which all the discrete techniques accumulated in the community of formal verification readily apply. This venture is mathematically supported by *nonstandard analysis*, where we can rigorously speak about infinites and infinitesimals.

In the talk I will lay out: 1) our framework of a while-language and a Hoare-style program logic, augmented with an infinitesimal constant, for modeling and verification of hybrid systems; 2) how discrete verification techniques can be *transferred*, as they are, to hybrid applications, via the celebrated *transfer principle* in nonstandard analysis; and 3) the overview of our prototype automatic prover.

The talk is based on the joint work with Kohei Suenaga, Kyoto University. References:

[1] Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling. Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.

[2] Ichiro Hasuo and Kohei Suenaga. Exercises in Nonstandard Static Analysis of Hybrid Systems. To appear in Proc. CAV 2012.