TY - GEN
T1 - Programming and Verifying Component Ensembles
AU - De Nicola, Rocco
AU - Lluch Lafuente, Alberto
AU - Loreti, Michele
AU - Morichetta, Andrea
AU - Pugliese, Rosario
AU - Senni, Valerio
AU - Tiezzi, Francesco
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-642-54848-2_5
DO - 10.1007/978-3-642-54848-2_5
M3 - Article in proceedings
SN - 978-3-642-54847-5
T3 - Lecture Notes in Computer Science
SP - 69
EP - 83
BT - From Programs to Systems. The Systems perspective in Computing
PB - Springer
T2 - ETAPS Workshop, FPS 2014
Y2 - 6 April 2014 through 6 April 2014
ER -