Verifying state reachability in a statechart model having computer program code embedded therein

摘要

Disclosed is method and system for verifying reachability of the states in a statechart model, where the statechart model is the combination statecharts and programmed instructions. The statechart model is transcribed into a first program code in a first programming language. Static analysis is performed upon the first program code to generate a master program code. The master program code comprises only information required for verifying reachability of the statechart model. The master program code is further translated into a second program code. Both, the master program code and the second program code is collated with a set of functions to generate first target program code and the second target program code respectively, where the set of functions are configured to encode an execution framework. Further, the execution framework is configured for verifying the reachability of the states in the statechart model by using "Simulation-based technique" and/or a "Model-based technique".