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. © 2014 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
De Nicola, R., Lluch Lafuente, A., Loreti, M., Morichetta, A., Pugliese, R., Senni, V., & Tiezzi, F. (2014). Programming and verifying component ensembles. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8415 LNCS, pp. 69–83). Springer Verlag. https://doi.org/10.1007/978-3-642-54848-2_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
