Abstract
We propose a compositional specification theory for reasoning about components that interact by synchronisation of input and output (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a theory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predicate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspondence between the operational and declarative frameworks.
Keywords
References
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)
de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26, 109–120 (2001)
Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why are modalities good for Interface Theories? In: Proc. 9th International Conference on Application of Concurrency to System Design, ACSD 2009, pp. 119–127. IEEE Computer Society (2009)
Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal Interfaces: Unifying Interface Automata and Modal Specifications. In: Proc. 7th International Conference on Embedded Software, EMSOFT 2009, pp. 87–96. ACM (2009)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2, 219–246 (1989)
Lüttgen, G., Vogler, W.: Conjunction on processes: Full abstraction via ready-tree semantics. Theor. Comput. Sci. 373, 19–40 (2007)
Lüttgen, G., Vogler, W.: Ready simulation for concurrency: It’s logical! Inf. Comput. 208, 845–867 (2010)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31, 560–599 (1984)
de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, T. (eds.) Engineering Theories of Software Intensive Systems. NATO Science Series II: Mathematics, Physics and Chemistry, vol. 195, pp. 83–104. Springer, Heidelberg (2005)
de Alfaro, L.: Game Models for Open Systems. In: Dershowitz, N. (ed.) Verification (Manna Festschrift). LNCS, vol. 2772, pp. 269–289. Springer, Heidelberg (2004)
Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: Proc. 8th ACM International Conference on Embedded Software, EMSOFT 2008, pp. 79–88. ACM (2008)
Bhaduri, P., Ramesh, S.: Interface synthesis and protocol conversion. Form. Asp. Comput. 20, 205–224 (2008)
Nicola, R.D., Segala, R.: A process algebraic view of input/output automata. Theor. Comput. Sci. 138, 391–423 (1995)
Tretmans, J.: Model-Based Testing and Some Steps towards Test-Based Modelling. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 297–326. Springer, Heidelberg (2011)
Josephs, M.B.: Receptive process theory. Acta Inf. 29, 17–31 (1992)
Josephs, M.B., Kapoor, H.K.: Controllable delay-insensitive processes. Fundam. Inf. 78, 101–130 (2007)
Raclet, J.B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M.: A Compositional Specification Theory for Component Behaviours. Technical Report RR-12-01, Department of Computer Science, University of Oxford (2012)
van Glabbeek, R.J.: Full abstraction in structural operational semantics (extended abstract). In: Proceedings of the Third International Conference on Methodology and Software Technology: Algebraic Methodology and Software Technology, pp. 75–82. Springer, Heidelberg (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, T., Chilton, C., Jonsson, B., Kwiatkowska, M. (2012). A Compositional Specification Theory for Component Behaviours. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)