Simulation-verification: biting at the state explosion problem


Douglas A. Stuart, Monica Brockmeyer, Aloysius K. Mok, Farnam Jahanian

IEEE Transactions on Software Engineering 27(7), pages 599-617, July 2001
IEEE Computer Sosciety

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.

 @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}

Tags:

Publication

— authors

Douglas A. Stuart, Monica Brockmeyer, Aloysius K. Mok, Farnam Jahanian

— status

published

— sort

article in journal

Venue

— journal

IEEE Transactions on Software Engineering

— volume

27

— issue

7

— pages

599-617

— publication date

July 2001

Identifiers

— DOI

10.1109/32.935853

— print ISSN

0098-5589

BibTeX

— BibTeX ID
stuart2001
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY