Programming and Verifying Component Ensembles

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

doi:10.1007/978-3-642-54848-2_5

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 proceeding › Article in proceedings › Research › peer-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 language	English
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
Publisher	Springer
Publication date	2014
Pages	69-83
ISBN (Print)	978-3-642-54847-5
ISBN (Electronic)	978-3-642-54848-2
DOIs	https://doi.org/10.1007/978-3-642-54848-2_5
Publication status	Published - 2014
Externally published	Yes
Event	ETAPS Workshop, FPS 2014 - Grenoble, France Duration: 6 Apr 2014 → …

Conference

Conference	ETAPS Workshop, FPS 2014
Country/Territory	France
City	Grenoble
Period	06/04/2014 → …

Series	Lecture Notes in Computer Science
Volume	8415
ISSN	0302-9743

Access to Document

10.1007/978-3-642-54848-2_5

Cite this

De Nicola, R., Lluch Lafuente, A., Loreti, M., Morichetta, A., Pugliese, R., Senni, V., & Tiezzi, F. (2014). Programming and Verifying Component Ensembles. In From Programs to Systems. The Systems perspective in Computing: ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings (pp. 69-83). Springer. Lecture Notes in Computer Science Vol. 8415 https://doi.org/10.1007/978-3-642-54848-2_5

De Nicola, Rocco ; Lluch Lafuente, Alberto ; Loreti, Michele ; Morichetta, Andrea ; Pugliese, Rosario ; Senni, Valerio ; Tiezzi, Francesco. / Programming and Verifying Component Ensembles. From Programs to Systems. The Systems perspective in Computing: ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Springer, 2014. pp. 69-83 (Lecture Notes in Computer Science, Vol. 8415).

@inproceedings{a2ab66d3588b478c90d328204863919a,

title = "Programming and Verifying Component Ensembles",

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.",

author = "{De Nicola}, Rocco and {Lluch Lafuente}, Alberto and Michele Loreti and Andrea Morichetta and Rosario Pugliese and Valerio Senni and Francesco Tiezzi",

year = "2014",

doi = "10.1007/978-3-642-54848-2_5",

language = "English",

isbn = "978-3-642-54847-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "69--83",

booktitle = "From Programs to Systems. The Systems perspective in Computing",

note = "ETAPS Workshop, FPS 2014 ; Conference date: 06-04-2014",

}

De Nicola, R, Lluch Lafuente, A, Loreti, M, Morichetta, A, Pugliese, R, Senni, V & Tiezzi, F 2014, Programming and Verifying Component Ensembles. in From Programs to Systems. The Systems perspective in Computing: ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Springer, Lecture Notes in Computer Science, vol. 8415, pp. 69-83, ETAPS Workshop, FPS 2014, Grenoble, France, 06/04/2014. https://doi.org/10.1007/978-3-642-54848-2_5

Programming and Verifying Component Ensembles. / De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco.

From Programs to Systems. The Systems perspective in Computing: ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Springer, 2014. p. 69-83 (Lecture Notes in Computer Science, Vol. 8415).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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

ER -

De Nicola R, Lluch Lafuente A, Loreti M, Morichetta A, Pugliese R, Senni V et al. Programming and Verifying Component Ensembles. In From Programs to Systems. The Systems perspective in Computing: ETAPS Workshop, FPS 2014, in Honor of Joseph Sifakis, Grenoble, France, April 6, 2014. Proceedings. Springer. 2014. p. 69-83. (Lecture Notes in Computer Science, Vol. 8415). https://doi.org/10.1007/978-3-642-54848-2_5

Programming and Verifying Component Ensembles

Abstract

Conference

Access to Document

Fingerprint

Cite this