Construction of Asynchronous Communicating Systems: Weak Termination Guaranteed!

摘要

Correctness ofasynchronously communicating systems (ACS) is known to be a hard problem, which became even more actual after the introduction of Service Oriented Architectures and Service Oriented Computing. In this paper, we focus on one particular correctness property, namely weak termination: at any moment of the system execution, at least one option to terminate should be available. We present a compositional method for constructing an ACS that guarantees weak termination. The method allows for refinement of single components, refinement of compositions of components and the creation of new components in the system. For two important classes of ACS, weak termination follows directly from their structure. These classes focus on the concurrency over components and on the implementation of protocols and communicating choices.