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

Abstract

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
PublisherSpringer
Publication date2014
Pages69-83
ISBN (Print)978-3-642-54847-5
ISBN (Electronic)978-3-642-54848-2
DOIs
Publication statusPublished - 2014
Externally publishedYes
EventETAPS Workshop, FPS 2014 - Grenoble, France
Duration: 6 Apr 2014 → …

Conference

ConferenceETAPS Workshop, FPS 2014
Country/TerritoryFrance
CityGrenoble
Period06/04/2014 → …
SeriesLecture Notes in Computer Science
Volume8415
ISSN0302-9743

Fingerprint

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

Cite this