TY - JOUR
T1 - An Algebraic Theory Of Boundary Crossing Transitions
JF - Electronic Notes in Theoretical Computer Science
Y1 - 2005
A1 - Ray,Arnab
A1 - Cleaveland, Rance
A1 - Skou,Arne
KW - Compositional Semantics
KW - Formal Methods
KW - Process algebra
KW - Statecharts
AB - 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.
VL - 115
SN - 1571-0661
UR - http://www.sciencedirect.com/science/article/pii/S1571066104053186
M3 - 10.1016/j.entcs.2004.09.029
ER -