Programming and verifying component ensembles. A simplified version of the kernel language SCEL, that we call SCELlight, is introduced as a formalism for programming and verifying properties of so-called cyber-physical systems consisting of software-intensive ensembles of components, featuring complex intercommunications and interactions with humans and other systems. In order to validate the amenability of the language for verification purposes, we provide a translation of SCELlight specifications into Promela. We test the feasibility of the approach by formally specifying an application scenario, consisting of a collection of components offering a variety of services meeting different quality levels, and by using SPIN to verify that some desired behaviors are guaranteed.
Keywords for this software
References in zbMATH (referenced in 4 articles )
Showing results 1 to 4 of 4.
- De Nicola, Rocco; Ferrari, Gianluigi; Pugliese, Rosario; Tiezzi, Francesco: A formal approach to the engineering of domain-specific distributed systems (2020)
- Hennicker, Rolf; Klarl, Annabelle; Wirsing, Martin: Model-checking \textscHelenaensembles with Spin (2015)
- Montanari, Ugo; Pugliese, Rosario; Tiezzi, Francesco: Programming autonomic systems with multiple constraint stores (2015)
- De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)