Model-Checking Helena Ensembles with Spin. 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 . 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Hennicker, Rolf: Role-based development of dynamically evolving esembles (2019)
- Viroli, Mirko; Beal, Jacob; Damiani, Ferruccio; Audrito, Giorgio; Casadei, Roberto; Pianini, Danilo: From distributed coordination to field calculus and aggregate computing (2019)
- Hennicker, Rolf; Klarl, Annabelle; Wirsing, Martin: Model-checking \textscHelenaensembles with Spin (2015)
- Hölzl, Matthias; Koch, Nora; Mayer, Philip; Schroeder, Andreas; Belzner, Lenz; Busch, Marianne; Fasching, Anton; Klarl, Annabelle; Kroiss, Christian; Raed, Laith: Ode to the PST (2015)
- Hennicker, Rolf; Klarl, Annabelle: Foundations for ensemble modeling -- the Helena approach. Handling massively distributed systems with elaborate ensemble architectures (2014)
- Klarl, Annabelle; Mayer, Philip; Hennicker, Rolf: \textschelena@work: modeling the science cloud platform (2014) ioport