Model-checking HELENA ensembles with spin

Abstract

The Helena approach allows to specify dynamically evolving ensembles of collaborating components. It is centered around the notion of roles which components can adopt in ensembles. In this paper, we focus on the early verification of Helena models. We propose to translate Helena specifications into Promela and check satisfaction of LTL properties with Spin [11]. To prove the correctness of the translation, we consider an SOS semantics of (simplified variants of) Helena and Promela and establish stutter trace equivalence between them. Thus, we can guarantee that a Helena specification and its Promela translation satisfy the same LTL formulae (without next). Our correctness proof relies on a new, general criterion for stutter trace equivalence.