Abstract
De Alfaro and Henzinger’s Interface Automata (IA) and Nyman et al.’s recent combination IOMTS of IA and Larsen’s Modal Transition Systems (MTS) are established frameworks for specifying interfaces of system components. However, neither IA nor IOMTS consider conjunction that is needed in practice when a component satisfies multiple interfaces, while Larsen’s MTS-conjunction is not closed. In addition, IOMTS-parallel composition exhibits a compositionality defect.
This paper defines conjunction on IA and MTS and proves the operators to be ‘correct’, i.e., the greatest lower bounds wrt. IA- and resp. MTS-refinement. As its main contribution, a novel interface theory called Modal Interface Automata (MIA) is introduced: MIA is a rich subset of IOMTS, is equipped with compositional parallel and conjunction operators, and allows a simpler embedding of IA than Nyman’s. Thus, it fixes the shortcomings of related work, without restricting designers to deterministic interfaces as Raclet et al.’s modal interface theory does.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM TOPLAS 1(3), 507–534 (1995)
Bauer, S., Hennicker, R., Wirsing, M.: Interface theories for concurrency and data. Theoret. Comp. Sc. 412(28), 3101–3121 (2011)
Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On Weak Modal Compatibility, Refinement, and the MIO Workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: FSE, pp. 109–120. ACM (2001)
de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-Intensive Systems. NATO Science Series, vol. 195. Springer (2005)
Fecher, H., de Frutos-Escrig, D., Lüttgen, G., Schmidt, H.: On the Expressiveness of Refinement Settings. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 276–291. Springer, Heidelberg (2010)
Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)
Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O Automata for Interface and Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007)
Larsen, K.G., Steffen, B., Weise, C.: A Constraint Oriented Proof Methodology Based on Modal Transition Systems. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 17–40. Springer, Heidelberg (1995)
Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. J. Logic Comput. 1(6), 761–795 (1991)
Lüttgen, G., Vogler, W.: Ready simulation for concurrency: It’s logical! Inform. and Comput. 208, 845–867 (2010)
Raclet, J., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 107, 1–32 (2011)
Schäfer, M., Vogler, W.: Component refinement and CSC-solving for STG decomposition. Theoret. Comp. Sc. 388(1-3), 243–266 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Lüttgen, G., Vogler, W. (2012). Modal Interface Automata. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds) Theoretical Computer Science. TCS 2012. Lecture Notes in Computer Science, vol 7604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33475-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-33475-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33474-0
Online ISBN: 978-3-642-33475-7
eBook Packages: Computer ScienceComputer Science (R0)