Simulation-verification: biting at the state explosion problem

• Published in: IEEE transactions on software engineering 2001-07, Vol.27 (7), p.599-617
• Main Authors: Stuart, D.A., Brockmeyer, M., Mok, A.K., Jahanian, F.
• Format: Article
• Language: English
• Subjects: Analytical models; Computation; Computational modeling; Computer simulation; Context modeling; Costs; Explosions; Graphs; Program verification (computers); Pulp manufacturing; Real time systems; Robot control; Robotic assembly; Robots; Specification languages; Specifications
• ISSN: 0098-5589
• DOI: 10.1109/32.935853

Simulation and verification are 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 due to the state-space explosion problem. 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 computation graph to that set of computations consistent with the simulation. This limited computation graph, called a simulation-verification graph, can be one or more orders of magnitude smaller than the full computation graph. A tool, XSVT, is described which implements simulation-verification graphs. Three paradigms for using the new technique are proposed. The paper illustrates the application of the proposed technique via an example of a robot controller for a manufacturing assembly line.