A generalised theory of Interface Automata, component compatibility and error

Original Article
First Online:
Received:
Accepted:

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.

This is a preview of subscription content, log in to check access

Notes

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.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24–53 (2016)MathSciNetCrossRefMATHGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Caillaud, B.: Mica: A modal interface compositional analysis library, 2011. http://www.irisa.fr/s4/tools/mica/. Last Accessed 27 Jan 2017
  10. 10.
    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)Google Scholar
  11. 11.
    Chilton, C.: An Algebraic Theory of Componentised Interaction. Ph.D. thesis, Oxford University (2013)Google Scholar
  12. 12.
    Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Technical report RR-13-02, Oxford University (2013)Google Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE), pp. 109–120. ACM (2001)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT-Press, Cambridge (1989)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Fendrich, S.: Modal Interface Theories for Specifying Component-based Systems. Ph.D. thesis, Bamberg University (2017)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    Gareis, J.: Prototypical Integration of the Modal Interface Automata Theory in Google Go. Master’s thesis, Bamberg University (2015)Google Scholar
  21. 21.
    Goessler, G., Raclet, J.-B.: Modal contracts for component-based design. In: Software Engineering and Formal Methods (SEFM), pp. 295–303. IEEE (2009)Google Scholar
  22. 22.
    Hennicker, R., Knapp, A.: Moving from interface theories to assembly theories. Acta Inform. 52(2–3), 235–268 (2015)MathSciNetCrossRefMATHGoogle Scholar
  23. 23.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)MATHGoogle Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, Volume 407 of LNCS, pp. 232–246. Springer, Berlin (1989)Google Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    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)Google Scholar
  28. 28.
    Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Logic in Computer Scienc (LICS), pp. 108–117. IEEE (1990)Google Scholar
  29. 29.
    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)Google Scholar
  30. 30.
    Lüttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inform. 52(4–5), 305–336 (2015)MathSciNetCrossRefMATHGoogle Scholar
  31. 31.
    Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATHGoogle Scholar
  32. 32.
    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)MathSciNetMATHGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Software Technologies Research GroupUniversity of BambergBambergGermany

Personalised recommendations