An Algebraic Theory Of Boundary Crossing Transitions

TitleAn Algebraic Theory Of Boundary Crossing Transitions
Publication TypeJournal Articles
Year of Publication2005
AuthorsRay A, Cleaveland R, Skou A
JournalElectronic Notes in Theoretical Computer Science
Pagination69 - 88
Date Published2005/01/18/
ISBN Number1571-0661
KeywordsCompositional Semantics, Formal Methods, Process algebra, Statecharts

This paper gives a process-algebraic semantics for the hierarchical state machine (HSM) fragment of Statecharts, in which state transitions are permitted to cross state boundaries. Although frowned upon by researchers as promoting unstructured modeling, such transitions are used extensively in practice to model parameterized start states and conditional exit states. The purpose of this work is to develop a compositional semantics for HSMs that may be fit together with compositional semantic accounts for Statecharts without boundary-crossing transitions in order to arrive at a compositional theory for virtually the whole Statecharts language. Our technical development consists of a process algebra for HSMs that is equipped with an operational semantics, an argument that bisimulation is a congruence for the algebra, a syntax-directed translation procedure for HSMs into the process algebra, and an equational axiomatization of the algebra.