Published: 19th August 2015
DOI: 10.4204/EPTCS.189
ISSN: 2075-2180

EPTCS 189

Proceedings 8th
Interaction and Concurrency Experience
Grenoble, France, 4-5th June 2015

Edited by: Sophia Knight, Ivan Lanese, Alberto Lluch Lafuente and Hugo Torres Vieira

Preface
Invited Presentation: Rigorous System Design
Joseph Sifakis
1
Invited Presentation: The importance and potential of descriptions to our industry
Steve Ross-Talbot
2
Relating BIP and Reo
Kasper Dokter, Sung-Shik Jongmans, Farhad Arbab and Simon Bliudze
3
Orchestrated Session Compliance
Franco Barbanera, Steffen van Bakel and Ugo de'Liguoro
21
Executable Behaviour and the π-Calculus (extended abstract)
Bas Luttik and Fei Yang
37
Analysis of Petri Nets and Transition Systems
Eike Best and Uli Schlachter
53
Reversible Barbed Congruence on Configuration Structures
Clément Aubert and Ioana Cristescu
68
The LTS WorkBench
Alceste Scalas and Massimo Bartoletti
86
On the Expressiveness of Joining
Thomas Given-Wilson and Axel Legay
99
On the Computation Power of Name Parameterization in Higher-order Processes
Xian Xu, Qiang Yin and Huan Long
114
Deductive Verification of Parallel Programs Using Why3
César Santos, Francisco Martins and Vasco Thudichum Vasconcelos
128

Preface

This volume contains the proceedings of ICE'15, the 8th Interaction and Concurrency Experience, which was held in Grenoble, France on the 4th and 5th of June 2015 as a satellite event of DisCoTec'15. 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), DisCoTec'13 (Florence, Italy), and DisCoTec'14 (Berlin, Germany).

The ICE workshop series has a main distinguishing aspect: the workshop features a particular review and selection procedure. 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 discussion forum with access restricted to the authors and to all the PC members not declaring a conflict of interest. The PC members post comments and questions to which the authors reply. Like in the past seven editions, the forum discussion during the review and selection phase of ICE'15 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 misspelled 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 9 papers, including 1 short paper, were accepted for publication (the workshop also featured 4 brief announcements which are not part of this volume). We were proud to host three invited talks, by Leslie Lamport (shared with the FRIDA workshop), Joseph Sifakis and Steve Ross-Talbot. The abstracts of the last two talks 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 Leslie Lamport, Joseph Sifakis and Steve Ross-Talbot for accepting our invitations to present their recent work, and the DisCoTec'15 organizers, in particular the general and workshop chairs, for providing an excellent environment for the preparation and staging of the event. Finally, we thank the editors of EPTCS for the publication of this post-proceedings and the sponsors of the event, namely we acknowledge support by Microsoft Research - INRIA Joint Centre.


Sophia Knight -- CNRS, LORIA, Université de Lorraine (France)
Ivan Lanese -- Focus Team, University of Bologna/INRIA (Italy)
Alberto Lluch Lafuente -- DTU Compute, Technical University of Denmark (Denmark)
Hugo Torres Vieira -- IMT Institute for Advanced Studies Lucca (Italy)

Rigorous System Design

Joseph Sifakis (RiSD laboratory, EPFL)

Abstract

The most important trend in ICT is the increasing integration of devices and services. The Internet of Things vision, born from the convergence between embedded and network technologies, aims at producing services addressing global challenges and societal needs. It involves devices interconnected through a unified network infrastructure to the cloud, for intelligent resource management and adaptation to quick changes.

No need to be a wizard to realize that this vision cannot come true, under current conditions. The main roadblocks to its achievement are poor dependability of infrastructures and systems, as well as impossibility to guarantee response times in communication. These are crucial requirements for the development of autonomous services for the management of critical resources and processes. Unfortunately, with the exception of a few well-regulated areas, e.g. avionics, the majority of systems are poorly engineered.

For those who have ever dealt with critical systems, it is obvious that cybercrime will never be mastered if we do not radically change the way we design and develop systems. There is no miracle. If we do not even understand how a system is built, it will never be possible to guarantee its trustworthiness.

The current situation is the result of the conjunction of at least three factors. Research in computer science has failed to provide relevant theory for rigorous system development. The existing infrastructures have been developed mostly in an ad hoc and incremental manner. Finally, even whenever it was technically feasible, authorities failed to promote regulatory policies for the quality of ICT products.

Today, the development costs of high confidence systems explode with their size. We are far away from the solution of the so called, software crisis. In fact, the latter hides another much bigger: the system crisis.

In my talk I will discuss rigorous system design as a formal and accountable process leading from requirements to correct-by-construction implementations. I will also discuss current limitations of the state of the art and advocate a coherent scientific foundation for system design based on four principles: 1) separation of concerns; 2) component-based construction; 3) semantic coherency; 4) correctness-by-construction. The combined application of these principles allows the definition of a methodology clearly identifying where human intervention and ingenuity are needed to resolve design choices, as well as activities that can be supported by tools to automate tedious and error-prone tasks.

The presented view for rigorous system design has been amply implemented in the BIP (Behavior, Interaction, Priority) component framework and substantiated by numerous experimental results showing both its relevance and feasibility.

I will conclude with a discussion advocating a system-centric vision for computing, and a deeper interaction and cross-fertilization with other more mature scientific disciplines.


The importance and potential of descriptions to our industry

Steve Ross-Talbot (ZDLC Business Unit, Cognizant Technology Solutions)

Abstract

Descriptions are a fundamental artefact of our industry. We embrace many of them, use them day to day, and rely on them for almost every aspect of life. We call them, collectively, programming languages. They have precision, some are higher level, enabling higher abstract concepts to be expressed in ways that are closer to the language of the domain, and others, whilst being turing complete, do not carry the syntactic sugar of a domain but are no less influenced by their surroundings and comfort zones. This plethora of descriptions live in a context of connectivity in which one description somehow passes information to another description that have entirely different syntaxes. It has become increasingly difficult for descriptions above this programming level to be kept up to date as a body of IT knowledge that, in part, expresses some of the genes of an enterprise or organization. With work on session types and work on other form of descriptions uncovering new things all of the time the Zero Deviation Lifecycle (ZDLC), in part borne on the wings of scribble [1], has been pioneering the automation of IT Knowledge with the aim of documenting the IT systems of the world. With an increase in regulations (Basel II) and a drive to focus resources on business innovation, saving money on the one hand and investing on the other, requires that IT knowledge is up to date to ensure good decision and policy making. Never before has the need for good descriptions of systems and their common collaborative behaviours been more important. This talk walks us through a journey towards our dream of true automated IT Knowledge connected to the systems that they describe and highlights the importance in terms of the use cases that are driving it forward.

References

  1. Nobuko Yoshida, Raymond Hu, Rumyana Neykova & Nicholas Ng (2013): The Scribble Protocol Language. In Martín Abadi & Alberto Lluch-Lafuente, editors: Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, Lecture Notes in Computer Science 8358, Springer, pp. 22-41. Available at http://dx.doi.org/10.1007/978-3-319-05119-2_3.