Science of Computer Programming, 170:49–79
January 2019 · doi: 10.1016/j.scico.2018.10.005
Statecharts are one of the most popular modeling formalisms that is used in a diversity of real world applications, such as cyber-physical systems, mobile computing, and bio-informatics. Following common step-wise refinement strategies, modelers often develop and evolve Statecharts models incrementally to satisfy requirements and changes. Although there are already several existing Statecharts refinement approaches, they provide insufficient guarantees to support reasoning about the preservation of both its internal structure, to enhance development and maintenance, and its behavior, which external components using the Statecharts model may depend on. In this paper, we formulate formal requirements to minimally limit the allowable Statecharts refinement operations such that certain assumptions on the structure and reachability of the Statecharts model will hold. To satisfy these requirements, we propose a set of practical bounding refinement rules that allows the modeler to achieve such refinements for which notions of behavior and structure preservation can be statically verified under some assumptions. Our implementation shows how these rules can be applied in realistic scenarios.
subject terms: Statechart, Refinement, Software design, Verification, Model-based Systems Engineering, MbSE