Abstract
Components are strongly encapsulated behaviours which interact with the environment by exchanging messages. Interaction may, amongst others, follow a synchronous rendezvous mechanism for message exchange or an asynchronous paradigm where sending and handling a message happens at different points in time. We extend our previously defined component model by integrating synchronous and asynchronous communication. As the formal background we use I/O-transition systems and consider asynchronous communication with fifo-ordered message buffers. We identify compatibility properties that should be satisfied when components communicate along synchronous and asynchronous connectors. As a first result we show that synchronous compatibility is a sufficient condition to ensure buffered compatibility in asynchronous communications. We introduce the notion of connection-safe assemblies which requires compatibility of both kinds of communication. We define a refinement relation and show its compositionality with respect to synchronous and asynchronous connectors in connection-safe assemblies. Finally, we provide results showing the preservation of connection-safety under component refinement.
This research has been partially supported by the GLOWA-Danube project (01LW0602A2) sponsored by the German Federal Ministry of Education and Research.
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.
References
Lau, K.K., Wang, Z.: Software Component Models. IEEE Trans. Softw. Eng. 33(10), 709–724 (2007)
Rausch, A., Reussner, R., Mirandola, R., Plášil, F. (eds.): The Common Component Modeling Example. LNCS, vol. 5153. Springer, Heidelberg (2008)
Hennicker, R., Janisch, S., Knapp, A.: On the Observable Behaviour of Composite Components. In: Proc. 5th Int. Wsh. Formal Aspects of Component Software, FACS 2008 (2008), http://www.pst.ifi.lmu.de/veroeffentlichungen/hennicker-et-al:facs:2008.pdf
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)
Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting Families of Software Systems with Process Algebras. ACM Trans. Softw. Eng. Meth. 11(4), 386–426 (2002)
Brim, L., Černá, I., Vařeková, P., Zimmerova, B.: Component-Interaction Automata as a Verification-Oriented Component-Based System Specification. SIGSOFT Softw. Eng. Notes 31(2), 1–8 (2006)
Brand, D., Zafiropulo, P.: On Communicating Finite-State Machines. J. ACM 30(2), 323–342 (1983)
Jéron, T., Jard, C.: Testing for Unboundedness of Fifo Channels. Theo. Comp. Sci. 113, 93–117 (1993)
Maréchal, O., Poizat, P., Royer, J.C.: Checking Asynchronously Communicating Components Using Symbolic Transition Systems. In: Meersman, R., Tari, Z. (eds.) OTM 2004. LNCS, vol. 3291, pp. 1502–1519. Springer, Heidelberg (2004)
Poizat, P., Royer, J.C.: A Formal Architectural Description Language based on Symbolic Transition Systems and Temporal Logic. J. Univ. Comp. Sci. 12(12), 1741–1782 (2006)
Hacklinger, F.: Java/A – Taking Components into Java. In: Proc. 13th ISCA Int. Conf. Intelligent and Adaptive Systems and Software Engineering (IASSE 2004), ISCA, pp. 163–169 (2004)
Ahumada, S., Apvrille, L., Barros, T., Cansado, A., Madelaine, E., Salageanu, E.: Specifying Fractal and GCM Components with UML. In: 26th Int. Conf. Chilean Computer Science Society (SCCC 2007), pp. 53–62. IEEE, Los Alamitos (2007)
Barros, T., Boulifa, R., Madelaine, E.: Parameterized Models for Distributed Java Objects. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 43–60. Springer, Heidelberg (2004)
Rajamani, S.K., Rehof, J.: Conformance Checking for Models of Asynchronous Message Passing Software. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 166–179. Springer, Heidelberg (2002)
Cécé, G., Finkel, A.: Verification of Programs with Half-Duplex Communication. Inform. Comp. 202(2), 166–190 (2005)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Gouda, M.G., Manning, E.G., Yu, Y.T.: On the Progress of Communications between Two Finite State Machines. Inform. Contr. 63(3), 200–216 (1984)
Larsen, K.G., Nyman, U., Wasowski, A.: Interface Input/Output Automata. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 82–97. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hennicker, R., Janisch, S., Knapp, A. (2010). Refinement of Components in Connection-Safe Assemblies with Synchronous and Asynchronous Communication. In: Choppy, C., Sokolsky, O. (eds) Foundations of Computer Software. Future Trends and Techniques for Development. Monterey Workshop 2008. Lecture Notes in Computer Science, vol 6028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12566-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-12566-9_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12565-2
Online ISBN: 978-3-642-12566-9
eBook Packages: Computer ScienceComputer Science (R0)