A Parametric Structural Operational Semantics for Stateflow, UML Statecharts, and Rhapsody

Associated research group: Critical Systems Research GroupIn this report, we define a parametric structural operational semantics that can be used to define the behavior of three Statecharts variants: Stateflow from the Mathworks, Inc., UML Statecharts from the Object Management Group, and Rhapsody from Rational/IBM Corporation. These dialects are the most commonly used variants of Statecharts in industrial applications, and are increasingly used to construct safety-critical applications. We believe that our semantics for each dialect is more complete than prior research and matches the informal documentation of each notation more closely than other approaches. In the formalization process, we have discovered deep similarities between the semantics, and we are able to create a parametric operational semantics that factors out the variabilities between the dialects in a modular way