Dynamic Slicing of Statechart Specifications for Reactive Systems

This paper extends the well-known technique of dynamic slicing to State chart specifications of reactive systems. 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 State chart specifications. In this paper, we firstly formally define a formal semantics model -- observable semantics, which only describes outside observable behavior and conceals unobservable behavior of State chart specifications. Then we propose a new notion of dynamic slicing that is more natural for State chart 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.