Establishing Properties of Interaction Systems

We exhibit sufficient conditions for generic properties of component based systems. The model we use to describe component based systems is the formalism of interaction systems. Because the state space explosion problem is encountered in interaction systems (i.e., an exploration of the state space gets unfeasible for a large number of components), we follow the guideline that these conditions have to be checkable efficiently (i.e., in time polynomial in the number of components). Further, the conditions are designed in such a way that the information gathered is reusable if a condition is not satisfied. Concretely, we consider deadlock-freedom and progress in interaction systems. We state a sufficient condition for deadlock-freedom that is based on an architectural constraint: We define what it means for an interaction system to be tree-like, and we derive a sufficient condition for deadlock-freedom of such systems. Considering progress, we first present a characterization of this property. Then we state a sufficient condition for progress which is based on a directed graph. We combine this condition with the characterization to point out one possibility to proceed if the graph-criterion does not yield progress. Both sufficient conditions can be checked efficiently because they only require the investigation of certain subsystems. Finally, we consider the effect that failure of some parts of the system has on deadlock-freedom and progress. We define robustness of deadlock-freedom respectively progress under failure, and we explain how the sufficient conditions above have to be adapted in order to be also applicable in this new situation