Radomski, Stefan ; Neubacher, Tim ; Schnelle-Walka, Dirk (2014)
From Harel To Kripke: A Provable Datamodel for SCXML.
EICS2014 Engineering Interactive Systems with SCXML Workshop Proceedings.
Konferenzveröffentlichung, Bibliographie
Kurzbeschreibung (Abstract)
When writing critical applications, developers need a way to formally prove that the resulting system complies to a set of constraints and exposes a specified behavior. With SCXML being a markup language for Harel state-charts, there is an untapped possibility to reduce the expressiveness of its embedded datamodel to enable model-checking techniques. In this paper we introduce a Promela datamodel for SCXML documents, enabling to transform these documents onto input files for the SPIN model-checker. By retaining most of the semantics, developers can prove various properties of systems expressed via SCXML documents employing this datamodel.
| Typ des Eintrags: | Konferenzveröffentlichung |
|---|---|
| Erschienen: | 2014 |
| Autor(en): | Radomski, Stefan ; Neubacher, Tim ; Schnelle-Walka, Dirk |
| Art des Eintrags: | Bibliographie |
| Titel: | From Harel To Kripke: A Provable Datamodel for SCXML |
| Sprache: | Englisch |
| Publikationsjahr: | Juni 2014 |
| Veranstaltungstitel: | EICS2014 Engineering Interactive Systems with SCXML Workshop Proceedings |
| Kurzbeschreibung (Abstract): | When writing critical applications, developers need a way to formally prove that the resulting system complies to a set of constraints and exposes a specified behavior. With SCXML being a markup language for Harel state-charts, there is an untapped possibility to reduce the expressiveness of its embedded datamodel to enable model-checking techniques. In this paper we introduce a Promela datamodel for SCXML documents, enabling to transform these documents onto input files for the SPIN model-checker. By retaining most of the semantics, developers can prove various properties of systems expressed via SCXML documents employing this datamodel. |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik > Telekooperation 20 Fachbereich Informatik |
| Hinterlegungsdatum: | 30 Apr 2015 11:39 |
| Letzte Änderung: | 30 Apr 2015 11:39 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum