| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Formalizing Statecharts using Hierarchical Automata
| Title: | Formalizing Statecharts using Hierarchical Automata |
| Authors: | Steffen Helke (helke /at/ cs /dot/ tu-berlin /dot/ de) and Florian Kammüller (flokam /at/ cs /dot/ tu-berlin /dot/ de) |
| Submission date: | 2010-08-08 |
| Abstract: | We formalize in Isabelle/HOL the abtract syntax and a synchronous step semantics for the specification language Statecharts. The formalization is based on Hierarchical Automata which allow a structural decomposition of Statecharts into Sequential Automata. To support the composition of Statecharts, we introduce calculating operators to construct a Hierarchical Automaton in a stepwise manner. Furthermore, we present a complete semantics of Statecharts including a theory of data spaces, which enables the modelling of racing effects. We also adapt CTL for Statecharts to build a bridge for future combinations with model checking. However the main motivation of this work is to provide a sound and complete basis for reasoning on Statecharts. As a central meta theorem we prove that the well-formedness of a Statechart is preserved by the semantics. |
| BibTeX: |
@article{Statecharts-AFP,
author = {Steffen Helke and Florian Kammüller},
title = {Formalizing Statecharts using Hierarchical Automata},
journal = {Archive of Formal Proofs},
month = aug,
year = 2010,
note = {\url{https://isa-afp.org/entries/Statecharts.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |