Simulation vs. verification: getting the best of both worlds

Simulation and verification are the two conventional techniques for the analysis of specifications of real-time systems. While simulation is relatively inexpensive in terms of execution time, it only validates the behavior of a system for one particular computation path. On the other hand, verification provides guarantees over the entire set of computation paths of a system, but is, in general, very expensive, i.e. it suffers from the state-space explosion problem. In this paper, we introduce a new technique: simulation-verification combines the best of both worlds by synthesizing an intermediate analysis method. This method uses simulation to limit the generation of a simulation-verification graph to that set of computations which is consistent with the simulation. A tool called XSVT (X Windows-based Simulation-Verification Tool) is described which implements simulation-verification graphs. Three paradigms for using the new technique are proposed