Simulation-verification: Biting at the state explosion problem

Simulation and verification are the two conventional techniques for the ana lysis of specifications of real-time systems. While simulation is relativel y inexpensive in terms of execution time, it only validates the behavior of a system for one particular computation path. On the other hand, verificat ion provides guarantees over the entire set of computation paths of a syste m. but is, in general. very expensive due to the state-space explosion prob lem. In this paper, we introduce a new technique: Simulation-verification c ombines the best of both worlds by synthesizing an intermediate analysis me thod. This method uses simulation to limit the generation of a computation graph to that set of computations consistent with the simulation. This limi ted computation graph, called a simulation-verification graph, can be one o r 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 t he application of the proposed technique via an example of a robot controll er for a manufacturing assembly line.