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 verication of Helena models. We propose to translate Helena specications into Promela and check satisfaction of LTL properties with Spin [11]. To prove the correctness of the translation, we consider an SOS semantics of (simplied variants of) Helena and Promela and establish stutter trace equivalence between them. Thus, we can guarantee that a Helena specication and its Promela translation satisfy the same LTL formulae (without next). Our correctness proof relies on a new, general criterion for stutter trace equivalence.

• Type: Journal
• Year: 2015
• Where: BIRTHDAY
• Authors: Rolf Hennicker, Annabelle Klarl, Martin Wirsing
• Keywords: Applied Computing, BIRTHDAY 2015