College of XingZhi, Zhejiang Normal University Jinhua, China

---

Abstract—This paper extends the well-known technique of dynamic slicing to Statechart specifications of reactive systems. Statechart language extends state machines along hierarchy, concurrency and communication – resulting in a compact visual notation that allows engineers to structure and modularize system descriptions. Dynamic slicing is well known in the domain of sequential transformational programs and has been found to be useful in understanding, analysis and verification. The classical definition of dynamic slicing is unsuitable for Statechart specifications. In this paper, we firstly formally define a formal semantics model -- observable semantics, which is very suitable for dynamic slicing, because that it only describes outside observable behavior and conceals unobservable behavior of Statechart specifications, and it fully captures the run-time dependence relation among the state transitions in the Statechart specification. Then we propose a new notion of dynamic slicing that, in our opinion, is more natural for Statechart specifications. We formally define notions of dynamic slicing criterion, dynamic slice and minimal dynamic slice, and we also explain how to produce valid dynamic slicing criterion and propose a simple and practical approximation algorithm for minimal dynamic slice generation using observable semantics as an intermediate representation.

Index Terms—Statechart Specification; Slicing; Slice Criterion; Specification analysis; Specification Verification; State Explosion Problem; Formal Semantics; Reactive Systems

[PDF]

Cite: Chunyu Miao, "Dynamic Slicing Research of UML Statechart Specifications," Journal of Computers vol. 6, no. 4, pp. 792-798, 2011.