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.
|Title of host publication||From Programs to Systems. The Systems perspective in Computing : ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings|
|Publication status||Published - 2014|
|Event||ETAPS Workshop, FPS 2014 - Grenoble, France|
Duration: 6 Apr 2014 → …
|Conference||ETAPS Workshop, FPS 2014|
|Period||06/04/2014 → …|
|Series||Lecture Notes in Computer Science|