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 -