Jump to : Abstract | Contact | BibTex reference | EndNote reference |
The analysis of programs by the exhaustive inspection of reachable states in a finite state graph is a well-understood procedure. It is straightforwardly applicable to many description languages and is actually implemented in several industrial tools. But one of the main limitations of today's verification tools is the size of the memory needed to exhaustively build the state graphs of the programs. For numerous properties, it is not necessary to explicitly build this graph and an exhaustive depth-first traversal is often sufficient. This leads to an on-line algorithms for computing Büchi acceptance (in the de terministic case) and behavioral equivalences: they are presented in detail. In order to avoid retraversing states, it is however important to store some of the already visited states in memory. To keep the memory size bounded (and avoid a performance falling down), visited states are randomly replaced. In most cases this depth-first traversal with replacement can push back significantly the limits of verification tools. We call ``on-the-fly verification'', the use of algorithms based on a depth-first search (with replacement) of the finite state graph associated with the program to be verified.
Thierry Jéron
Thierry.Jeron@irisa.fr
@article{Fernandez-Jard-Jeron-Mounier-FMSD93,
Author = {Fernandez, J.-C. and Jard, C. and Jéron, T. and Mounier, L.},
Title = {On-the-fly Verification of Finite Transition Systems},
Journal = {Formal Methods in System Design},
Volume = {1},
Number = {2},
Pages = {251--273},
Publisher = {Kluwer Academic Publishers},
Year = {1992}
}
Get EndNote Reference (.ref)