Abstract
Treating control and data in an integrated way is an important issue in system development. We discuss a compositional approach for specifying concurrent behavior of components with data states on the basis of interface theories. The dynamic aspects of a system are specified by modal I/O-transition systems, whereas changes of data states are specified by pre- and postconditions. In this setting we study refinement and behavioral compatibility of components. We show that refinement is compositional and that compatibility is preserved by refinement; thus the requirements for interface theories are satisfied. As a consequence, our approach supports independent implementability and reusability of concurrently interacting components with data states.
This work has been partially sponsored by the EU project ASCENS, 257414. The first author has been partially supported by the German Academic Exchange Service (DAAD), grant D/10/46169.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Brückner, B., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL: the Common Algebraic Specification Language. Theor. Comput. Sci. 286(2), 153–196 (2002)
Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed fractal components. Annales des Télécommunications 64(1-2), 25–43 (2009)
Bauer, S.S., Hennicker, R., Bidoit, M.: A modal interface theory with data constraints. In: Davies, J., Davies, J., Silva, L., Simão, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 80–95. Springer, Heidelberg (2011)
Bauer, S.S., Hennicker, R., Wirsing, M.: Interface theories for concurrency and data. Theor. Comput. Sci. 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)
Bergstra, J.A., Middelburg, C.A.: An interface group for process components. Fundam. Inform. 99(4), 355–382 (2010)
Cengarle, M.V., Knapp, A., Mühlberger, H.: Interactions. In: Lano, K. (ed.) UML 2 Semantics and Applications, pp. 205–248 (2009)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)
de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable Interfaces. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 81–105. Springer, Heidelberg (2005)
de Alfaro, L., Henzinger, T.A.: Interface Theories for Component-Based Design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)
Ehrig, H., Claßen, I., Boehm, P., Fey, W., Korff, M., Löwe, M.: Algebraic Concepts for Software Development in ACT ONE, ACT TWO and LOTOS (eingeladener Vortrag). In: Lippe, W.-M. (ed.) Software-Entwicklung. Informatik-Fachberichte, vol. 212, pp. 201–224. Springer, Heidelberg (1989)
Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 2. EATCS Monographs of Theoretical Computer Science, vol. 21. Springer, Berlin (1990)
Fernandes, F., Royer, J.-C.: The STSLib project: Towards a formal component model based on STS. Electr. Notes Theor. Comput. Sci. 215, 131–149 (2008)
Fischer, C.: CSP-OZ: a combination of Object-Z and CSP. In: Bowman, H., Derrick, J. (eds.) Proc. FMOODS, Canterbury, UK, pp. 423–438. Chapman and Hall, London (1997)
Goguen, J.A., Kirchner, C., Kirchner, H., Mégrelis, A., Meseguer, J., Winkler, T.C.: An Introduction to OBJ 3. In: Kaplan, S., Jouannaud, J.-P. (eds.) CTRS 1987. LNCS, vol. 308, pp. 258–263. Springer, Heidelberg (1988)
Harel, D., Thiagarajan, P.S.: Message sequence charts. In: Lavagno, L., Martin, G., Selic, B. (eds.) UML for Real: Design of Embedded Real-time Systems. Kluwer Academic Publishers (2003)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271–281 (1972)
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., Thomsen, B.: A Modal Process Logic. In: 3rd Annual Symp. Logic in Computer Science, LICS 1988, pp. 203–210. IEEE Computer Society (1988)
Montesi, F., Sangiorgi, D.: A Model of Evolvable Components. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010, LNCS, vol. 6084, pp. 153–171. Springer, Heidelberg (2010)
Mouelhi, S., Chouali, S., Mountassir, H.: Refinement of interface automata strengthened by action semantics. Electr. Notes Theor. Comput. Sci. 253(1), 111–126 (2009)
Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why Are Modalities Good for Interface Theories? In: 9th Int. Conf. Application of Concurrency to System Design, ACSD 2009, pp. 119–127. IEEE Computer Society, Los Alamitos (2009)
Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 451–470. Springer, Heidelberg (2002)
Sannella, D., Wirsing, M.: A Kernel Language for Algebraic Specification and Implementation. In: Karpinski, M. (ed.) FCT 1983. LNCS, vol. 158, pp. 413–427. Springer, Heidelberg (1983)
Wirsing, M.: Algebraic Specification. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 675–788 (1990)
Wirsing, M.: Algebraic Specification Languages: An Overview. In: Astesiano, E., Reggio, G., Tarlecki, A. (eds.) Abstract Data Types 1994 and COMPASS 1994. LNCS, vol. 906, pp. 81–115. Springer, Heidelberg (1995)
Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
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
Bauer, S.S., Hennicker, R., Wirsing, M. (2012). Building a Modal Interface Theory for Concurrency and Data. In: Mossakowski, T., Kreowski, HJ. (eds) Recent Trends in Algebraic Development Techniques. WADT 2010. Lecture Notes in Computer Science, vol 7137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28412-0_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-28412-0_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28411-3
Online ISBN: 978-3-642-28412-0
eBook Packages: Computer ScienceComputer Science (R0)