Statecharts disentangled

We present some of the main results of the research obtained by Benjamin De Leeuw in his PhD thesis: ”Statechart DNA: Formal and Psychological Investigation into a State Machine Theory”. The Simplified Statechart language was derived by excluding all redundant constructs of the UML (Unified Modeling Language) metamodel on statecharts. Simplified state machines and their memory model are the central abstraction used throughout this work. Any UML state machine or procedural program transforms to exactly one simplified state machine. The language grammar for simplified state machines was derived by composing a scripting language that further abstracts any useful state machine. Each grammar rule gets a visual counterpart within the state machine diagram. All useful state machines can be ”grown” from these scripts. The parse tree of this grammar can be normalized such that any state machine has exactly one script, called statechart dna. In this paper we concentrate on an execution model for simplified statecharts, and graft on these semantics a useful technique for (temporal) value propagation. We determine the values of all variables in the reachable and useful states of the simplified statechart. Hence we can check for temporal properties on each of the executions of simplified statecharts, by modeling the possible values in a Kripke Model and applying model checking techniques on it.

ISBN:9789604741786

Publication year:2010

Accessibility:Closed