Programming and Verifying Component Ensembles

Rocco De Nicola, Alberto Lluch Lafuente, Michele Loreti, Andrea Morichetta, Rosario Pugliese, Valerio Senni, Francesco Tiezzi

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationFrom Programs to Systems. The Systems perspective in Computing : ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings
Publication date2014
ISBN (Print)978-3-642-54847-5
ISBN (Electronic)978-3-642-54848-2
Publication statusPublished - 2014
Externally publishedYes
EventETAPS Workshop, FPS 2014 - Grenoble, France
Duration: 6 Apr 20146 Apr 2014


ConferenceETAPS Workshop, FPS 2014
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Programming and Verifying Component Ensembles'. Together they form a unique fingerprint.

Cite this