Proceedings Fourth Workshop on
Edited by: Sebastian Bauer and Jean-Baptiste Raclet
Foundations of Interface Technologies
Tallinn, Estonia, 25th March 2012
Component-based design is widely considered as a major approach to
developing systems in a time and cost effective way. Central in this
approach is the notion of an interface. Interfaces summarize the
externally visible properties of a component and are seen as a key to
achieving component interoperability and to predict global system
behavior based on the component behavior. To capture the intricacy of
complex software products, rich interfaces have been proposed. These
interfaces do not only specify syntactic properties, such as the
signatures of methods and operations, but also take into account
behavioral and extra-functional properties, such as quality of
service, security and dependability. Rich interfaces have been
proposed for describing, e.g., the legal sequences of messages or
method calls accepted by components, or the resource and timing
constraints in embedded software. The development of a rigorous
framework for the specification and analysis of rich interfaces is
challenging. This area of research has been recently acknowledged
when the seminal paper Interface Automata written in 2001 by
Luca de Alfaro and Thomas
A. Henzinger received the 2011 ACM SIGSOFT Impact Paper Award.
FIT stands for Foundations of Interface Technologies. The aim of this
workshop is to bring together researchers who are interested in the
formal underpinnings of interface technologies. Previous occurrences
of FIT took place in 2005 (satellite workshop of CONCUR, in San
Francisco, CA, USA), in 2008 (satellite workshop of ETAPS, in
Budapest, Hungary) and in 2010 (satellite workshop of CONCUR, in
Paris, France). The fourth occurrence of FIT was collocated with ETAPS
2012 in Tallinn, Estonia, and took place on March 25, 2012. The
workshop program consisted of nine talks including three contributed
talks and six invited talks. The present proceedings contain two papers
of contributed talks and three papers of invited talks.
Contributed talks have been selected by the program committee listed
- Sebastian Bauer (LMU München, Germany), co-chair
- Jean-Baptiste Raclet (University Toulouse III, France), co-chair
- Tevfik Bultan (University of California, Santa Barbara, USA)
- Marco Faella (Università di Napoli "Federico II", Italy)
- Rolf Hennicker (LMU München, Germany)
- Holger Hermanns (Saarland University, Germany)
- Kim G. Larsen (Aalborg University, Denmark)
- Axel Legay (INRIA/IRISA Rennes, France)
- Thomas Santen (Microsoft Research, Germany)
- Sven Schewe (University of Liverpool, UK)
- Mariëlle Stoelinga (University of Twente, The Netherlands)
- Andrzej Wąsowski (IT University Copenhagen, Denmark)
The papers appearing in the proceedings present the most recent trends
in interface technologies. In particular, two contributions discuss
expressive specification formalisms on the basis of modal transition
systems as stepping stones for rich interface theories: the invited
contribution by Srba considers various extensions of modal transition
systems while the invited paper by Legay introduces robust
specification theories with a quantitative approach to system
refinement. The invited paper by Traonouez presents results about the
robust implementability of a real-time interacting system. The
contributed paper by Carbone et al. defines transition systems with
response constraints, and the contributed paper by La Torre et al.
interfaces to the sequentialization of parametrized programs.
We would like to thank all authors of the papers in these proceedings as well as the following authors for their presentations at the workshop:
- José Luiz Fiadeiro (An Interface and Component Algebra for Service-Oriented Design)
- Karsten Wolf (Show me your friends and I tell you who you are)
- Oana Andrei, Muffy Calder and Alice Miller (Role-based Interface Automata)
- Rolf Hennicker (Challenges and Solutions in Interface-Based Design of Component Systems)
Finally, our thanks also goes to the organizers of ETAPS 2012 for their support in the organization of this workshop.
March 2012, Sebastian Bauer and Jean-Baptiste Raclet
Jiří Srba (Aalborg University)
Modal transition systems have recently attracted a considerable attention, mainly due to their
simple and intuitive semantics and many desirable properties needed for a step-wise refinement
process in the development of software components. Nevertheless, with respect to the actual modelling
expressiveness, the formalism allows to describe systems at a rather low abstraction level.
We have recently worked on different extensions of modal transitions to overcome some of their
limitations and we shall present a selection of our ideas, namely, the extensions of the formalism
with structured labels, and parametric and dual-priced modal transition systems.
Modal Transition Systems (MTS), a specification formalism originally proposed by Larsen and Thomsen 
in 1988, has been recently applied to interface theories [32, 31, 3, 31, 30, 2], verification of product
lines [20, 24, 27], program analysis [19, 21, 28] and other areas [14, 23, 16, 11, 12, 15, 5]. A tool
support is currently also under development [6, 17, 13, 7].
The MTS formalism is appealing due to its simplicity and the possibility to capture the essence of
process refinement: to enforce a presence of certain actions in all refined specifications we use must
transitions, while the presence of other actions can be optional and depicted using the may transitions.
The refinement now essentially reduces to iteratively resolving the status of may transitions: either by
removing them or by turning them into must transitions.
On the other hand, the classical MTS formalism has a limited expressive power for modelling of certain
phenomena. Consider, for example, a specification of a traffic light where after the red light the system
allows to enter either directly the green light (like at a pedestrian crossing) or first the yellow light
followed by the green light (like at a traffic light for the cars). When the red light is on, the choice
between going to green or yellow can be typically modelled using may transitions, however, this causes
some problems. A concrete implementation may then choose to implement both or none of the two options,
in any of these cases giving us an ill-behaved traffic light implementation. Similarly, the choices between
going to green or yellow cannot be settled in a persistent way as the next time the traffic light enters
the red light, its behaviour may change. Several extensions like disjunctive MTS , 1-selecting MTS 
and transition systems with obligations  give partial solutions to these problems. In our recent work 
we unified such attempts and introduced parametric modal transition systems, the theory of which we
Another limitation of the MTS formalism is the treatment of transition labels as in the classical setting
there is no support for label refinement. As an example, we may want to specify a machine accepting coins
and providing drinks. This can be modelled using a loop consisting of two transitions, the first one being
a may transition that accepts a coin, followed by a must transition returning a drink. A tea machine and
a coffee machine can be thought of as the obvious implementations of our generic coin-drink machine,
however, this cannot be captured using the standard modal refinement relation as
here the concrete implementation labels, like tea and coffee, are required to be present already at
its high-level specification. We have developed a framework that allows for a label refinement in
weighted and multi-weighted modal transition systems  and further unified the ideas into a general
theory of label-structured modal transition systems . This enables us to prove results dealing
with e.g. parallel composition, conjunction and quotienting, important operators for a sound
compositional reasoning, and these general results specialize to the subclasses of already studied variants
of modal transition systems. We shall present the basic ideas behind label-structured MTS and discuss
the applicability of the theory. For further general approaches focusing on compositionality we refer
the reader to [29, 11, 30].
Finally, the MTS theory should be also capable of expressing constraints for several non-functional
properties such as timing, energy-consumption and band-width. In our recent work [22, 1], the
MTS framework has been extended to allow for the specification of additional constraints on
quantitative aspects (e.g. time, power or memory) that are highly relevant in the area of embedded systems,
including the work on dual-priced MTS  where we continue the pursuit of quantitative extensions
of MTS by presenting an MTS with time durations modelled as controllable or uncontrollable intervals
and we equip the model with two kinds of quantitative aspects: each action has its own running cost
per time unit, and actions may require several hardware components of different costs. Then we ask the
question, given a fixed budget for the investment into the hardware components, what is the
implementation with the cheapest long-run average reward. We shall discuss this extension too.
S.S. Bauer, U. Fahrenberg, L. Juhl, K.G. Larsen, A. Legay & C.R. Thrane (2011):
Quantitative Refinement for Weighted Modal Transition Systems.
S.S. Bauer, R. Hennicker & M. Bidoit (2010):
A Modal Interface Theory with Data Constraints.
In: Jim Davies, Leila Silva & Adenilso da Silva Simão: SBMF,
S.S. Bauer, R. Hennicker & S. Janisch (2010):
Interface Theories for (A)synchronously Communicating Modal I/O-Transition Systems.
In: Axel Legay & Benoît Caillaud: FIT,
S.S. Bauer, L. Juhl, K.G. Larsen, A. Legay & J. Srba (2012):
Extending Modal Transition Systems with Structured Labels.
Mathematical Structures in Computer Science,
S.S. Bauer, K.G. Larsen, A. Legay, U. Nyman & A. Wasowski (2011):
A Modal Specification Theory for Components with Data.
In: Farhad Arbab & Peter Csaba Ölveczky: Proceedings of FACS 2011, 8th International Symposium on Formal Aspects of Component Software,
S.S. Bauer, Ph. Mayer & A. Legay (2011):
MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces.
In: Tevfik Bultan & Pao-Ann Hsiung: ATVA,
Available at http://anna.fi.muni.cz/~xbenes3/MoTraS/.
N. Beneš & J. Křetínský (2010):
Process Algebra for Modal Transition Systemses.
In: Ludek Matyska, Michal Kozubek, Tomás Vojnar, Pavel Zemcík & David Antos: MEMICS,
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany,
N. Beneš, J. Křetínský, K.G. Larsen, M.H. Møller & J. Srba (2011):
Parametric Modal Transition Systems.
In: Proceedings of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA'11),
N. Beneš, J. Křetínský, K.G. Larsen, M.H. Møller & J. Srba (2012):
Dual-Priced Modal Transition Systems with Time Durations.
In: Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12),
N. Bertrand, A. Legay, S. Pinchinat & J.-B. Raclet (2009):
A Compositional Approach on Modal Specifications for Timed Systems.
In: Karin Breitman & Ana Cavalcanti: ICFEM,
N. Bertrand, S. Pinchinat & J.-B. Raclet (2009):
Refinement and Consistency of Timed Modal Specifications.
In: Adrian Horia Dediu, Armand-Mihai Ionescu & Carlos Martín-Vide: LATA,
Mica: A Modal Interface Compositional Analysis Library.
Available at http://www.irisa.fr/s4/tools/mica/.
B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen & A. Wasowski (2010):
Compositional Design Methodology with Constraint Markov Chains.
In: Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST).
IEEE Computer Society,
A. David, K.G. Larsen, A. Legay, U. Nyman & A. Wasowski (2010):
Timed I/O automata: a complete specification theory for real-time systems.
In: Karl Henrik Johansson & Wang Yi: HSCC.
B. Delahaye, J.-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher & A. Wasowski (2011):
Abstract Probabilistic Automata.
In: Ranjit Jhala & David A. Schmidt: VMCAI,
N. D'Ippolito, D. Fischbein, M. Chechik & S. Uchitel (2008):
MTSA: The Modal Transition System Analyser.
H. Fecher & H. Schmidt (2008):
Comparing Disjunctive Modal Transition Systems with an One-Selecting Variant.
J. of Logic and Alg. Program. 77(1-2),
P. Godefroid, M. Huth & R. Jagadeesan (2001):
Abstraction-Based Model Checking Using Modal Transition Systems.
In: Proc. CONCUR'01,
A. Gruler, M. Leucker & K. D. Scheidemann (2008):
Modeling and Model Checking Software Product Lines.
In: Gilles Barthe & Frank S. de Boer: FMOODS,
M. Huth, R. Jagadeesan & D. A. Schmidt (2001):
Modal Transition Systems: A Foundation for Three-Valued Program Analysis.
In: Proc. of ESOP'01,
L. Juhl, K.G. Larsen & J. Srba (2011):
Modal Transition Systems with Weight Intervals.
Journal of Logic and Algebraic Programming.
. To appear..
J.-P. Katoen, D. Klink & M.R. Neuhäußer (2009):
Compositional Abstraction for Stochastic Systems.
In: Joël Ouaknine & Frits W. Vaandrager: FORMATS,
K. G. Larsen, U. Nyman & A. Wasowski (2007):
On Modal Refinement and Consistency.
In: Proc. of CONCUR'07,
K. G. Larsen & B. Thomsen (1988):
A Modal Process Logic.
IEEE Computer Society,
K. G. Larsen & L. Xinxin (1990):
Equation Solving Using Modal Transition Systems.
IEEE Computer Society,
K.G. Larsen, U. Nyman & A. Wasowski (2007):
Modal I/O Automata for Interface and Product Line Theories.
In: Rocco De Nicola: ESOP,
S. Nanz, F. Nielson & H. R. Nielson (2008):
Modal Abstractions of Concurrent Behaviour.
In: Proc. of SAS'08,
J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay & R. Passerone (2009):
Modal interfaces: unifying interface automata and modal specifications.
In: Proceedings of the seventh ACM international conference on Embedded software,
New York, NY, USA,
J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay & R. Passerone (2011):
A Modal Interface Theory for Component-Based Design.
Fundamenta Informaticae 108(1-2),
J.-B. Raclet, E. Badouel, A. Benveniste, B. Caillaud & R. Passerone (2009):
Why Are Modalities Good for Interface Theories?.
In: Application of Concurrency to System Design, 2009. ACSD '09. Ninth International Conference on,
pp. 119 –127,
S. Uchitel & M. Chechik (2004):
Merging partial behavioural models.
In: Proc. of FSE'04.