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 1 article )
Showing result 1 of 1.
- De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)