Modal interface theories for communication-safe component assemblies. (English) Zbl 1350.68182
Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2011. 8th international colloquium, Johannesburg, South Africa, August 31 – September 2, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23282-4/pbk). Lecture Notes in Computer Science 6916, 135-153 (2011).
Summary: We propose an extension of the abstract rules for independent implementability of reactive components proposed in interface theories to take into account interface assemblies. As a concrete instantiation we extend existing interface theories for modal I/O-transition systems to support assemblies, (greybox) assembly refinement and assembly encapsulation. We introduce a new notion of communication-safety for \(N\)-ary assemblies which overcomes problems with previous definitions of interface compatibility. We show that communication-safety can be checked incrementally. We also show that communication-safety is preserved by assembly refinement, that blackbox refinement of component interfaces is compositional w.r.t. greybox refinement of assemblies and, conversely, that assembly encapsulation maps greybox to blackbox refinement. The methodology of our approach is illustrated by a small case study.
For the entire collection see [Zbl 1229.68001].
For the entire collection see [Zbl 1229.68001].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Software:
MIO WorkbenchReferences:
| [1] | Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed Fractal components. Ann. Télécom. 64(1-2), 25–43 (2009) · doi:10.1007/s12243-008-0069-7 |
| [2] | 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) · Zbl 1284.68339 · doi:10.1007/978-3-642-12002-2_15 |
| [3] | Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting families of software systems with process algebras. ACM Trans. Softw. Eng. Methodol. 11(4), 386–426 (2002) · doi:10.1145/606612.606614 |
| [4] | Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983) · Zbl 0512.68039 · doi:10.1145/322374.322380 |
| [5] | Cerná, I., Vareková, P., Zimmerova, B.: Component substitutability via equivalencies of component-interaction automata. Electr. Notes Theor. Comput. Sci. 182, 39–55 (2007) · doi:10.1016/j.entcs.2006.09.030 |
| [6] | de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. 9th ACM SIGSOFT Ann. Symp. Foundations of Software Engineering (FSE 2001), pp. 109–120 (2001) · doi:10.1145/503209.503226 |
| [7] | de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Broy, M., Grünbauer, J., Harel, D., Hoare, C.A.R. (eds.) Engineering Theories of Software-intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195, pp. 83–104. Springer, Heidelberg (2005) · doi:10.1007/1-4020-3532-2_3 |
| [8] | Fernandes, F., Royer, J.-C.: The STSLib project: Towards a formal component model based on STS. Electr. Notes Th. Comp. Sci. 215, 131–149 (2008) · doi:10.1016/j.entcs.2008.06.025 |
| [9] | Hüttel, H., Larsen, K.G.: The use of static constructs in a modal process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989) · doi:10.1007/3-540-51237-3_14 |
| [10] | 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) · Zbl 1187.68296 · doi:10.1007/978-3-540-71316-6_6 |
| [11] | Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. 3rd Ann. Symp. Logic in Computer Science (LICS 1988), pp. 203–210. IEEE Computer Society, Los Alamitos (1988) |
| [12] | Plášil, F., Višňovský, S.: Behavior protocols for software components. IEEE Trans. Software Eng. 28(11), 1056–1076 (2002) · doi:10.1109/TSE.2002.1049404 |
| [13] | Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.): The Common Component Modeling Example. LNCS, vol. 5153. Springer, Heidelberg (2008) |
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.
