TU Darmstadt / ULB / TUbiblio

From Harel To Kripke: A Provable Datamodel for SCXML

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 Frage zum Eintrag

Optionen (nur für Redakteure)
Redaktionelle Details anzeigen Redaktionelle Details anzeigen