Simulation-verification: biting at the state explosion problem

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...

Full description

Saved in:
Bibliographic Details
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
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0098-5589
DOI:10.1109/32.935853