EPTCS 87
Proceedings Fourth Workshop on
Foundations of Interface Technologies
Tallinn, Estonia, 25th March 2012
Edited by: Sebastian Bauer and JeanBaptiste Raclet
Componentbased 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 extrafunctional 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
below:
 Sebastian Bauer (LMU München, Germany), cochair
 JeanBaptiste Raclet (University Toulouse III, France), cochair
 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 realtime interacting system. The
contributed paper by Carbone et al. defines transition systems with
response constraints, and the contributed paper by La Torre et al.
applies
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 ServiceOriented Design)
 Karsten Wolf (Show me your friends and I tell you who you are)
 Oana Andrei, Muffy Calder and Alice Miller (Rolebased Interface Automata)
 Rolf Hennicker (Challenges and Solutions in InterfaceBased 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 JeanBaptiste Raclet
Jiří Srba (Aalborg University)
Abstract
Modal transition systems have recently attracted a considerable attention, mainly due to their
simple and intuitive semantics and many desirable properties needed for a stepwise 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 dualpriced modal transition systems.
Overview
Modal Transition Systems (MTS), a specification formalism originally proposed by Larsen and Thomsen [25]
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 illbehaved 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 [26], 1selecting MTS [18]
and transition systems with obligations [8] give partial solutions to these problems. In our recent work [9]
we unified such attempts and introduced parametric modal transition systems, the theory of which we
shall present.
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 coindrink 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 highlevel specification. We have developed a framework that allows for a label refinement in
weighted and multiweighted modal transition systems [22] and further unified the ideas into a general
theory of labelstructured modal transition systems [4]. 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 labelstructured 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 nonfunctional
properties such as timing, energyconsumption and bandwidth. 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 dualpriced MTS [10] 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 longrun average reward. We shall discuss this extension too.
References

S.S. Bauer, U. Fahrenberg, L. Juhl, K.G. Larsen, A. Legay & C.R. Thrane (2011):
Quantitative Refinement for Weighted Modal Transition Systems.
In: MFCS,
LNCS 6907.
Springer,
pp. 60–71,
doi:10.1007/9783642229930_9.

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,
LNCS 6527.
Springer,
pp. 80–95,
doi:10.1007/9783642198298_6.

S.S. Bauer, R. Hennicker & S. Janisch (2010):
Interface Theories for (A)synchronously Communicating Modal I/OTransition Systems.
In: Axel Legay & Benoît Caillaud: FIT,
EPTCS 46,
pp. 1–8,
doi:10.4204/EPTCS.46.1.

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,
pp. 1–35.
To appear..

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,
LNCS.
Springer.
To appear.

S.S. Bauer, Ph. Mayer & A. Legay (2011):
MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces.
In: Tevfik Bultan & PaoAnn Hsiung: ATVA,
LNCS 6996.
Springer,
pp. 418–421,
doi:10.1007/9783642243721_30.

N. Beneš:
MoTraS.
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,
OASICS 16.
Schloss Dagstuhl  LeibnizZentrum fuer Informatik, Germany,
pp. 9–18,
doi:10.4230/OASIcs.MEMICS.2010.9.

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),
LNCS 6996.
SpringerVerlag,
pp. 275–289,
doi:10.1007/9783642243721_20.

N. Beneš, J. Křetínský, K.G. Larsen, M.H. Møller & J. Srba (2012):
DualPriced Modal Transition Systems with Time Durations.
In: Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'12),
LNCS 7180.
SpringerVerlag,
pp. 122–137,
doi:10.1007/9783642287176_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,
LNCS 5885.
Springer,
pp. 679–697,
doi:10.1007/9783642103735_35.

N. Bertrand, S. Pinchinat & J.B. Raclet (2009):
Refinement and Consistency of Timed Modal Specifications.
In: Adrian Horia Dediu, ArmandMihai Ionescu & Carlos MartínVide: LATA,
LNCS 5457.
Springer,
pp. 152–163,
doi:10.1007/9783642009822_13.

B. Caillaud:
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,
pp. 123–132,
doi:10.1109/QEST.2010.23.

A. David, K.G. Larsen, A. Legay, U. Nyman & A. Wasowski (2010):
Timed I/O automata: a complete specification theory for realtime systems.
In: Karl Henrik Johansson & Wang Yi: HSCC.
ACM,
pp. 91–100,
doi:10.1145/1755952.1755967.

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,
LNCS 6538.
Springer,
pp. 324–339,
doi:10.1007/9783642182754_23.

N. D'Ippolito, D. Fischbein, M. Chechik & S. Uchitel (2008):
MTSA: The Modal Transition System Analyser.
In: ASE.
IEEE,
pp. 475–476,
doi:10.1109/ASE.2008.78.

H. Fecher & H. Schmidt (2008):
Comparing Disjunctive Modal Transition Systems with an OneSelecting Variant.
J. of Logic and Alg. Program. 77(12),
pp. 20–39,
doi:10.1016/j.jlap.2008.05.003.

P. Godefroid, M. Huth & R. Jagadeesan (2001):
AbstractionBased Model Checking Using Modal Transition Systems.
In: Proc. CONCUR'01,
LNCS 2154.
Springer,
pp. 426–440,
doi:10.1007/3540446850_29.

A. Gruler, M. Leucker & K. D. Scheidemann (2008):
Modeling and Model Checking Software Product Lines.
In: Gilles Barthe & Frank S. de Boer: FMOODS,
LNCS 5051.
Springer,
pp. 113–131,
doi:10.1007/9783540688631_8.

M. Huth, R. Jagadeesan & D. A. Schmidt (2001):
Modal Transition Systems: A Foundation for ThreeValued Program Analysis.
In: Proc. of ESOP'01,
LNCS 2028.
Springer,
pp. 155–169,
doi:10.1007/3540453091_11.

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,
LNCS 5813.
Springer,
pp. 195–211,
doi:10.1007/9783642043680_16.

K. G. Larsen, U. Nyman & A. Wasowski (2007):
On Modal Refinement and Consistency.
In: Proc. of CONCUR'07,
LNCS 4703.
Springer,
pp. 105–119,
doi:10.1007/9783540744078_8.

K. G. Larsen & B. Thomsen (1988):
A Modal Process Logic.
In: LICS.
IEEE Computer Society,
pp. 203–210,
doi:10.1109/LICS.1988.5119.

K. G. Larsen & L. Xinxin (1990):
Equation Solving Using Modal Transition Systems.
In: LICS.
IEEE Computer Society,
pp. 108–117,
doi:10.1109/LICS.1990.113738.

K.G. Larsen, U. Nyman & A. Wasowski (2007):
Modal I/O Automata for Interface and Product Line Theories.
In: Rocco De Nicola: ESOP,
LNCS 4421.
Springer,
pp. 64–79,
doi:10.1007/9783540713166_6.

S. Nanz, F. Nielson & H. R. Nielson (2008):
Modal Abstractions of Concurrent Behaviour.
In: Proc. of SAS'08,
LNCS 5079.
Springer,
pp. 159–173,
doi:10.1007/9783540691662_11.

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,
EMSOFT '09.
ACM,
New York, NY, USA,
pp. 87–96,
doi:10.1145/1629335.1629348.

J.B. Raclet, E. Badouel, A. Benveniste, B. Caillaud, A. Legay & R. Passerone (2011):
A Modal Interface Theory for ComponentBased Design.
Fundamenta Informaticae 108(12),
pp. 119–149,
doi:10.3233/FI2011416.

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,
doi:10.1109/ACSD.2009.22.

S. Uchitel & M. Chechik (2004):
Merging partial behavioural models.
In: Proc. of FSE'04.
ACM,
pp. 43–52,
doi:10.1145/1041685.1029904.