Tim A. C. Willemse

Debjyoti Bera, Tim A. C. Willemse

Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clients). The high degree of concurrency in asynchronous communicating systems increases the risk of unintentionally introducing deadlocks and livelocks. The weak termination property serves as a basic sanity check to avoid such problems. It assures that in each reachable state, the system has the option to eventually terminate. This paper generalizes existing results that, by construction, guarantee weakly terminating interface compositions. Our generalizations make the theory applicable more broadly in practice. Starting with an interface specification of a server satisfying certain properties, we show how a class of clients modeling different usage contexts can be derived using a partial mirroring relation. Furthermore, we discuss an embedding of our results in an open-source tool to guide modelers in designing weakly terminating interfaces.

Neda Noroozi, Mohammad Reza Mousavi, Tim A. C. Willemse

We study the problem of deriving a specification for a third-party component, based on the specification of the system and the environment in which the component is supposed to reside. Particularly, we are interested in using component specifications for conformance testing of black-box components, using the theory of input-output conformance (ioco) testing. We propose and prove sufficient criteria for decompositionality, i.e., that components conforming to the derived specification will always compose to produce a correct system with respect to the system specification. We also study the criteria for strong decomposability, by which we can ensure that only those components conforming to the derived specification can lead to a correct system.