A generalised theory of Interface Automata, component compatibility and error
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.
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.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.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.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.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.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.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.Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24–53 (2016)MathSciNetCrossRefMATHGoogle Scholar
- 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.Caillaud, B.: Mica: A modal interface compositional analysis library, 2011. http://www.irisa.fr/s4/tools/mica/. Last Accessed 27 Jan 2017
- 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.Chilton, C.: An Algebraic Theory of Componentised Interaction. Ph.D. thesis, Oxford University (2013)Google Scholar
- 12.Chilton, C., Jonsson, B., Kwiatkowska, M.: An algebraic theory of interface automata. Technical report RR-13-02, Oxford University (2013)Google Scholar
- 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.de Alfaro, L., Henzinger, T.A.: Interface automata. In: Foundations of Software Engineering (FSE), pp. 109–120. ACM (2001)Google Scholar
- 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.Dill, D.L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT-Press, Cambridge (1989)Google Scholar
- 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.Fendrich, S.: Modal Interface Theories for Specifying Component-based Systems. Ph.D. thesis, Bamberg University (2017)Google Scholar
- 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.Gareis, J.: Prototypical Integration of the Modal Interface Automata Theory in Google Go. Master’s thesis, Bamberg University (2015)Google Scholar
- 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.Hennicker, R., Knapp, A.: Moving from interface theories to assembly theories. Acta Inform. 52(2–3), 235–268 (2015)MathSciNetCrossRefMATHGoogle Scholar
- 23.Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)MATHGoogle Scholar
- 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.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.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.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.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.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.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.Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATHGoogle Scholar
- 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