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 (T r ). Based on the candidate trace (T r ), the abstraction module generates an abstract model (M A ) 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 (M A ) for obtaining a trace (T A ) such that a set of transitions in the trace (T A ) 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.