×

Interface theories for concurrency and data. (English) Zbl 1216.68187

Summary: We present 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 input/output automata, whereas changing data states are specified by pre- and postconditions. The combination of the two formalisms leads to our notion of modal input/output automata with data constraints (MIODs). In this setting we study refinement and behavioral compatibility of MIODs. We show that compatibility is preserved by refinement and that refinement is compositional w.r.t. synchronous composition, thus satisfying basic requirements of an interface theory. We propose a semantic foundation of interface specifications where any MIOD is equipped with a model-theoretic semantics describing the class of its correct implementation models. Implementation models are formalized in terms of guarded input/output transition systems and the correctness notion is based on a simulation relation between an MIOD and an implementation model which relates not only abstract and concrete control states but also (abstract) data constraints and concrete data states. We show that our approach is compositional in the sense that locally correct implementation models of compatible MIODs compose to globally correct implementations, thus ensuring independent implementability.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barros, Tomás; Ameur-Boulifa, Rabéa; Cansado, Antonio; Henrio, Ludovic; Madelaine, Eric, Behavioural models for distributed fractal components, Annales des Télécommunications, 64, 1-2, 25-43 (2009)
[2] Sebastian S. Bauer, Rolf Hennicker, Michel Bidoit, A modal interface theory with data constraints, in: [3]; Sebastian S. Bauer, Rolf Hennicker, Michel Bidoit, A modal interface theory with data constraints, in: [3] · Zbl 1325.68055
[3] (Davies, Jim; Silva, Leila; Simão, Adenilso da Silva, Formal Methods: Foundations and Applications — 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers. Formal Methods: Foundations and Applications — 13th Brazilian Symposium on Formal Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6527 (2011), Springer) · Zbl 1213.68032
[4] Bauer, Sebastian S.; Hennicker, Rolf; Janisch, Stephan, Behaviour protocols for interacting stateful components, Electr. Notes Theoret. Comput. Sci., 263, 47-66 (2010)
[5] Bauer, Sebastian S.; Mayer, Philip; Schroeder, Andreas; Hennicker, Rolf, On weak modal compatibility, refinement, and the MIO Workbench, (Proc. TACAS 2010. Proc. TACAS 2010, Lect. Notes Comp. Sci., vol. 6015 (2010), Springer), 175-189 · Zbl 1284.68339
[6] Benes, Nikola; Kretínský, Jan; Guldstrand Larsen, Kim; Srba, Jirí, On determinism in modal transition systems, Theoret. Comput. Sci., 410, 41, 4026-4043 (2009) · Zbl 1186.68314
[7] Bergstra, Jan A.; Broy, Manfred; Tucker, J. V.; Wirsing, Martin, On the power of algebraic specifications, (Gruska, Jozef; Chytil, Michal, MFCS. MFCS, Lecture Notes in Computer Science, vol. 118 (1981), Springer), 193-204
[8] Bergstra, Jan A.; Middelburg, C. A., An interface group for process components, Fundam. Inform., 99, 4, 355-382 (2010) · Zbl 1204.68134
[9] Bidoit, Michel; Hennicker, Rolf; Knapp, Alexander; Baumeister, Hubert, Glass-box and black-box views on object-oriented specifications, (Proc. SEFM’04. Proc. SEFM’04, Beijing, China (2004), IEEE Comp. Society Press), 208-217
[10] Cengarle, Maria Victoria; Knapp, Alexander; Mühlberger, Heribert, Interactions, (Lano, Kevin, UML 2 Semantics and Applications (2009)), 205-248
[11] de Alfaro, Luca; da Silva, Leandro Dias; Faella, Marco; Legay, Axel; Roy, Pritam; Sorea, Maria, Sociable interfaces, (Gramlich, Bernhard, FroCos. FroCos, Lecture Notes in Computer Science, vol. 3717 (2005), Springer), 81-105 · Zbl 1171.68837
[12] de Alfaro, Luca; Henzinger, Thomas A., Interface automata, Software Eng. Notes, 109-120 (2001)
[13] Luca de Alfaro, Thomas A. Henzinger, Interface theories for component-based design, in: EMSOFT 2001, 2001, pp. 148-165.; Luca de Alfaro, Thomas A. Henzinger, Interface theories for component-based design, in: EMSOFT 2001, 2001, pp. 148-165. · Zbl 1050.68518
[14] de Alfaro, Luca; Henzinger, Thomas A., Interface-based Design, (Broy, Manfred; Grünbauer, Johannes; Harel, David; Hoare, C. A.R., Engineering Theories of Software-intensive Systems. Engineering Theories of Software-intensive Systems, NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195 (2005), Springer), 83-104
[15] Fernandes, Fabrício; Royer, Jean-Claude, The STSLib project: towards a formal component model based on STS, Electr. Notes Theoret. Comput. Sci., 215, 131-149 (2008)
[16] Fischer, Clemens, CSP-OZ: a combination of Object-Z and CSP, (Bowman, H.; Derrick, J., Proc. FMOODS. Proc. FMOODS, Canterbury, UK (1997), Chapman and Hall: Chapman and Hall London), 423-438
[17] Goguen, Joseph; Burstall, Rod, Institutions: abstract model theory for specification and programming, J. ACM, 39, 1, 95-146 (1992) · Zbl 0799.68134
[18] Harel, D.; Thiagarajan, P. S., Message sequence charts, (Lavagno, Luciano; Martin, Grant; Selic, Bran, UML for Real: Design of Embedded Real-time Systems (2003), Kluwer Academic Publishers) · Zbl 1187.68081
[19] Hoare, C. A.R., Proofs of correctness of data representations, Acta Inform., 1, 271-281 (1972) · Zbl 0244.68009
[20] Hans Hüttel, Kim Guldstrand Larsen, The use of static constructs in a modal process logic, in: Logic at Botik 1989, 1989, pp. 163-180.; Hans Hüttel, Kim Guldstrand Larsen, The use of static constructs in a modal process logic, in: Logic at Botik 1989, 1989, pp. 163-180.
[21] Larsen, Kim Guldstrand; Nyman, Ulrik; Wasowski, Andrzej, Modal I/O Automata for Interface and Product Line Theories, (ESOP 2007. ESOP 2007, LNCS, vol. 4421 (2007), Springer), 64-79 · Zbl 1187.68296
[22] Larsen, Kim Guldstrand; Nyman, Ulrik; Wasowski, Andrzej, On Modal Refinement and Consistency, (CONCUR 2007. CONCUR 2007, LNCS, vol. 4703 (2007), Springer), 105-119 · Zbl 1151.68541
[23] Larsen, Kim Guldstrand; Thomsen, Bent, A Modal Process Logic, (3rd Annual Symp. Logic in Computer Science, LICS 1988 (1988), IEEE Computer Society), 203-210
[24] Milner, Robin, (Communication and Concurrency. Communication and Concurrency, Prentice Hall (International Series in Computer Science) (1989))
[25] F. Montesi, D. Sangiorgi, A model of evolvable components, in: [26]; F. Montesi, D. Sangiorgi, A model of evolvable components, in: [26]
[26] (Wirsing, Martin; Hofmann, Martin; Rauschmayer, Axel, Trustworthly Global Computing — 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers. Trustworthly Global Computing — 5th International Symposium, TGC 2010, Munich, Germany, February 24-26, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol. 6084 (2010), Springer) · Zbl 1198.68071
[27] Mouelhi, Sebti; Chouali, Samir; Mountassir, Hassan, Refinement of interface automata strengthened by action semantics, Electr. Notes Theoret. Comput. Sci., 253, 1, 111-126 (2009)
[28] Raclet, Jean-Baptiste; Badouel, Eric; Benveniste, Albert; Caillaud, Benoît; Passerone, Roberto, Why Are Modalities Good for Interface Theories?, (9th Int. Conf. Application of Concurrency to System Design, ACSD 2009 (2009), IEEE Computer Society: IEEE Computer Society Los Alamitos, CA, USA), 119-127 · Zbl 1242.68147
[29] Sampaio, Augusto; Woodcock, Jim; Cavalcanti, Ana, Refinement in Circus, (Eriksson, Lars-Henrik; Lindsay, Peter A., FME. FME, Lecture Notes in Computer Science, vol. 2391 (2002), Springer), 451-470 · Zbl 1064.68539
[30] Wirsing, Martin, Algebraic specification, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (1990)), 675-788 · Zbl 0900.68309
[31] (Wirsing, Martin; Bergstra, Jan A., Algebraic Methods: Theory, Tools and Applications [papers from a Workshop in Passau, Germany, June 9-11, 1987]. Algebraic Methods: Theory, Tools and Applications [papers from a Workshop in Passau, Germany, June 9-11, 1987], Lecture Notes in Computer Science, vol. 394 (1989), Springer) · Zbl 0745.68019
[32] Woodcock, Jim; Cavalcanti, Ana, The semantics of Circus, (Bert, Didier; Bowen, Jonathan P.; Henson, Martin C.; Robinson, Ken, ZB. ZB, Lecture Notes in Computer Science, vol. 2272 (2002), Springer), 184-203 · Zbl 1044.68560
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.