Preface

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 below:

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

Beyond the Classical Modal Transition Systems

Abstract

Overview

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 [26], 1-selecting 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 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 [22] and further unified the ideas into a general theory of label-structured 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 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 [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 long-run average reward. We shall discuss this extension too.

References

1. 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/978-3-642-22993-0_9.
2. 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/978-3-642-19829-8_6.
3. 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, EPTCS 46, pp. 1–8, doi:10.4204/EPTCS.46.1.
4. 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..
5. 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.
6. 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, LNCS 6996. Springer, pp. 418–421, doi:10.1007/978-3-642-24372-1_30.
7. N. Beneš: MoTraS. Available at http://anna.fi.muni.cz/~xbenes3/MoTraS/.
8. 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 - Leibniz-Zentrum fuer Informatik, Germany, pp. 9–18, doi:10.4230/OASIcs.MEMICS.2010.9.
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. Springer-Verlag, pp. 275–289, doi:10.1007/978-3-642-24372-1_20.
10. 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), LNCS 7180. Springer-Verlag, pp. 122–137, doi:10.1007/978-3-642-28717-6_12.
11. 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/978-3-642-10373-5_35.
12. 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, LNCS 5457. Springer, pp. 152–163, doi:10.1007/978-3-642-00982-2_13.
13. B. Caillaud: Mica: A Modal Interface Compositional Analysis Library. Available at http://www.irisa.fr/s4/tools/mica/.
14. 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.
15. 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. ACM, pp. 91–100, doi:10.1145/1755952.1755967.
16. 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/978-3-642-18275-4_23.
17. 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.
18. H. Fecher & H. Schmidt (2008): Comparing Disjunctive Modal Transition Systems with an One-Selecting Variant. J. of Logic and Alg. Program. 77(1-2), pp. 20–39, doi:10.1016/j.jlap.2008.05.003.
19. P. Godefroid, M. Huth & R. Jagadeesan (2001): Abstraction-Based Model Checking Using Modal Transition Systems. In: Proc. CONCUR'01, LNCS 2154. Springer, pp. 426–440, doi:10.1007/3-540-44685-0_29.
20. 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/978-3-540-68863-1_8.
21. M. Huth, R. Jagadeesan & D. A. Schmidt (2001): Modal Transition Systems: A Foundation for Three-Valued Program Analysis. In: Proc. of ESOP'01, LNCS 2028. Springer, pp. 155–169, doi:10.1007/3-540-45309-1_11.
22. L. Juhl, K.G. Larsen & J. Srba (2011): Modal Transition Systems with Weight Intervals. Journal of Logic and Algebraic Programming. . To appear..
23. 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/978-3-642-04368-0_16.
24. 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/978-3-540-74407-8_8.
25. K. G. Larsen & B. Thomsen (1988): A Modal Process Logic. In: LICS. IEEE Computer Society, pp. 203–210, doi:10.1109/LICS.1988.5119.
26. 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.
27. 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/978-3-540-71316-6_6.
28. 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/978-3-540-69166-2_11.
29. 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.
30. 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), pp. 119–149, doi:10.3233/FI-2011-416.
31. 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.
32. S. Uchitel & M. Chechik (2004): Merging partial behavioural models. In: Proc. of FSE'04. ACM, pp. 43–52, doi:10.1145/1041685.1029904.