Limiting state space explosion of model checking using discrete event simulation: combining DEVS and PROMELA

In this paper we propose an approach combining discrete event simulation and model checking. Indeed, methods like model checking suffer from the state space explosion when the modeled system is complex. Consequently, we propose an approach that allows the model checking procedure to focus on a subset of the total state space that is more likely to contain an erroneous state regarding a property. To do so, a simulation run that allows us to observe some qualitative metrics is performed, and stopped when a predefined "critical state" is reached. This state is then projected as the initial state of the non-deterministic finite automaton used by the model checking procedure. Thus, the search will only explore states reachable from this critical state, limiting state space explosion. We finally illustrate the proposed approach through a Network-On-Chip system, and compare it with the ad hoc classical model checking approach.