Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Programming and Verifying Component Ensembles
verfasst von : Rocco De Nicola, Alberto Lluch Lafuente, Michele Loreti, Andrea Morichetta, Rosario Pugliese, Valerio Senni, Francesco Tiezzi
Erschienen in: From Programs to Systems. The Systems perspective in Computing
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.