Abstract
Interface theories allow system designers to reason about the composability and compatibility of concurrent system components. Such theories often extend both de Alfaro and Henzinger’s Interface Automata and Larsen’s Modal Transition Systems, which leads, however, to several issues that are undesirable in practice: an unintuitive treatment of specified unwanted behaviour, a binary compatibility concept that does not scale to multi-component assemblies, and compatibility guarantees that are insufficient for software product lines. In this article we show that communication mismatches are central to all these problems and, thus, the ability to represent such errors semantically is an important feature of an interface theory. Accordingly, we present the error-aware interface theory EMIA, where the above shortcomings are remedied by introducing explicit fatal error states. In addition, we prove via a Galois insertion that EMIA is a conservative generalisation of the established Modal Interface Automata theory.
Similar content being viewed by others
References
Bauer, S.S., David, A., Hennicker, R., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Moving from specifications to contracts in component-based design. In: Fundamental Approaches to Software Engineering (FASE), Volume 7212 of LNCS, pp. 43–58. Springer, Berlin (2012)
Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO Workbench. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6015 of LNCS, pp. 175–189. Springer, Berlin (2010)
Beneš, N., Černa, I., Křetiínský, J.: Disjunctive modal transition systems and generalized LTL model checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University Brno (2010)
Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A.: Hennessy-Milner logic with greatest fixed points as a complete behavioural specification theory. In: Concurrency Theory (CONCUR), Volume 8052 of LNCS, pp. 76–90. Springer, Berlin (2013)
Beyer, D., Chakrabarti, A., Henzinger, T.A., Seshia, S.A.: An application of web-service interfaces. In: International Conference on Web Services (ICWS), pp. 831–838. IEEE (2007)
Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. In: Theory and Practice of Computer Science (SOFSEM), Volume 8939 of LNCS, pp. 152–163. Springer, Berlin (2015)
Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24–53 (2016)
Bujtor, F., Vogler, W.: Error-pruning in interface automata. In: Theory and Practice of Computer Science (SOFSEM), Volume 8327 of LNCS, pp. 162–173. Springer, Berlin (2014)
Caillaud, B.: Mica: A modal interface compositional analysis library, 2011. http://www.irisa.fr/s4/tools/mica/. Last Accessed 27 Jan 2017
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.Z.: A compositional specification theory for component behaviours. In: Programming Languages and Systems (ESOP), Volume 7211 of LNCS, pp. 148–168. Springer, Berlin (2012)
Chilton, C.: An Algebraic Theory of Componentised Interaction. Ph.D. thesis, Oxford University (2013)
Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Technical report RR-13-02, Oxford University (2013)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE), pp. 109–120. ACM (2001)
de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-Intensive Systems, Volume 195 of NATO Science, pp. 83–104. Springer, Berlin (2005)
Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT-Press, Cambridge (1989)
Emmi, M., Giannakopoulou, D., Păsăreanu, C.S.: Assume-guarantee verification for interface automata. In: Formal Methods (FM), Volume 5014 of LNCS, pp. 116–131. Springer, Berlin (2008)
Fendrich, S.: Modal Interface Theories for Specifying Component-based Systems. Ph.D. thesis, Bamberg University (2017)
Fendrich, S., Lüttgen, G.: A generalised theory of interface automata, component compatibility and error. In: Integrated Formal Methods (iFM), Volume 9681 of LNCS, pp. 160–175. Springer, Berlin (2016)
Gareis, J.: Prototypical Integration of the Modal Interface Automata Theory in Google Go. Master’s thesis, Bamberg University (2015)
Goessler, G., Raclet, J.-B.: Modal contracts for component-based design. In: Software Engineering and Formal Methods (SEFM), pp. 295–303. IEEE (2009)
Hennicker, R., Knapp, A.: Moving from interface theories to assembly theories. Acta Inform. 52(2–3), 235–268 (2015)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)
Křetínský, J., Sickert, S.: MoTraS: a tool for modal transition systems and their extensions. In: Automated Technology for Verification and Analysis (ATVA), Volume 8172 of LNCS, pp. 487–491. Springer, Berlin (2013)
Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, Volume 407 of LNCS, pp. 232–246. Springer, Berlin (1989)
Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: Programming Languages and Systems (ESOP), Volume 4421 of LNCS, pp. 64–79. Springer, Berlin (2007)
Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 1019 of LNCS, pp. 17–40. Springer, Berlin (1995)
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Logic in Computer Scienc (LICS), pp. 108–117. IEEE (1990)
Lohstroh, M., Lee, E.A.: An interface theory for the Internet of Things. In: Software Engineering and Formal Methods (SEFM), Volume 9276 of LNCS, pp. 20–34. Springer, Berlin (2015)
Lüttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inform. 52(4–5), 305–336 (2015)
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)
Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1–2), 119–149 (2011)
Acknowledgements
We are grateful to Ferenc Bujtor, Rance Cleaveland, Rolf Hennicker, Kim G. Larsen, Michael Mendler, Thomas Streicher, Walter Vogler, Diedrich Wolter and the anonymous reviewers for their helpful suggestions.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Fendrich, S., Lüttgen, G. A generalised theory of Interface Automata, component compatibility and error. Acta Informatica 56, 287–319 (2019). https://doi.org/10.1007/s00236-018-0319-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00236-018-0319-8