Role-based development of dynamically evolving esembles

Abstract

An ensemble is a set of computing entities that collaborate to perform a certain task. Typically an ensemble changes dynamically its constitution such that new members can join and other members can leave an ensemble during its execution. The members of an ensemble interact through message exchange. They are modelled as instances of certain role types which can be adopted by components of an underlying component system. We propose a dynamic logic to describe the evolution of ensembles from a global perspective. Using the power of dynamic logic with diamond and box modalities over regular expressions of actions (involving role instance creation, message exchange and component access) we can specify safety and liveness properties as well as desired and forbidden interaction scenarios. Thus our approach is suitable to write formal requirements specifications for ensemble behaviours. For ensemble design and implementation we propose ensemble realisations. An ensemble realisation takes a local view by giving a constructive specification for each single role type in terms of a process algebraic expression. Correctness of an ensemble realisation is defined semantically: its generated ensemble transition system must be a model of the requirements specification. We consider bisimulation of ensemble transition systems and show that our approach enjoys the Hennessy-Milner property.