Behaviour Properties of Uniformly Parameterised Cooperations

In this paper we consider safety and liveness properties, where possibilistic aspects of especially liveness properties are captured by a modified satisfaction relation, called approximate satisfaction. The systems in focus of this paper are uniformly parameterised cooperations. Such systems are characterised by the composition of a set of identical components. These components interact in a uniform manner described by the schedules of the partners. Such kind of interaction is typical for scalable complex systems with cloud or grid structure. As a main result, a finite state verification framework for uniformly parameterised behaviour properties is given. The keys to this framework are structuring cooperations into phases and defining closed behaviours of systems. Finite state semi-algorithms that are independent of the concrete parameter setting are presented to verify behaviour properties of such uniformly parameterised cooperations.