Verifying Properties of Coordination by Well-Structured Transition Systems

Coordination models and languages are introduced to effectively rule and govern the interactions in those systems that feature complexity, distribution, opennes and high dynamics. These characteristics, however, traditionally impose a number of constraints on the engineering process: most notably, they make system specifications infinite, thus complicating - and sometimes preventing - the successful automatic verification of properties. In the field of verification for infinite state systems, the notion of well-structured transition systems has recently being introduced and studied. Its framework not only unifies a number of existing results in the context of infinite verification, but also introduces general concepts and methodologies, such as upward-closure and backward analysis, that show a great potential applicability for concurrent and interactive systems in general. In this paper, we evaluate the applicability of this framework to the context of coordination, formally defining the notion of well-structured coordination. A coordinated system adhering to this notion is amenable to a description in terms of a well-structured transition system, where interesting properties concerning termination, boundedness, safety, and liveness are decidable. An example of application to the Linda coordination model is studied, focussing on a methodology for proving the safety properties of coordinated systems.