Refinement of Components in Connection-Safe Assemblies with Synchronous and Asynchronous Communication

摘要

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.