TRACE BASED REACHABILITY ANALYSIS IN STATECHARTS

摘要

Disclosed is a method and system for verifying a statechart model (M) having one or more statecharts (S) and a set of traces (T). From the given set of traces (T), a designating module designates a trace as candidates trace (Tr). Based on the candidate trace (Tr), the abstraction module generates an abstract model (MA) by categorizing number of states of the each statechart (S) into at most three categories of states. Thereafter, the model checking module runs a bounded model checker (MC) upon the abstract model (MA) for obtaining a trace (TA) such that a set of transitions in the trace (TA) is a set of potentially transitions of a valid path for the unreached states in the statechart model (M). Further, a path concretization module verifies the reachability of the unreached states by incrementally constructing a concrete path using the potential transitions.