APICe » Publications » Simulation-verification: biting at the state explosion problem

Simulation-verification: biting at the state explosion problem

Douglas A. Stuart, Monica Brockmeyer, Aloysius K. Mok, Farnam Jahanian
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 due to 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 computation graph to that set of computations consistent with the simulation. This limited computation graph, called a simulationverification 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.
IEEE Transactions on Software Engineering 27(7), pages 599-617, july 2001, IEEE Computer Sosciety
@article{stuart2001,
title={Simulation-verification: biting at the state explosion problem},
author={Stuart, Douglas A. and Brockmeyer, Monica and Mok, Aloysius K. and Jahanian, Farnam},
journal={IEEE Transactions on Software Engineering},
year={2001},
month={july},
volume={27},
number={7},
pages={599--617},
doi={10.1109/32.935853},
ISSN={0098-5589},
publisher ={IEEE Computer Sosciety}
}