Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Gziped Postscript (.ps.gz)
Copyright noticeThis material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Model-checking is the basis of several verification tools. It allows to check if a finite state program satisfies a set of temporal logic formulas. The main limitation is the size of the memory needed to record the state graph. Avoiding state space explosion is necessary to improve the applicability of such verification tools. For that aim, we explore an approach called ``on-line model-checking" where satisfiability is checked during the state generation process. We deal with the simple context of checking finite computations against linear temporal logic properties. The logic specification is first translated into a finite automaton. This one values the system states during enumeration. Validity can be decided in finite time provided a memory larger than the state graph diameter. Precise algorithms and some results of experiments are given.
Thierry Jéron
Thierry.Jeron@irisa.fr
@InProceedings{Jard-Jeron-CAV89,
Author = {Jard, C. and Jéron, T.},
Title = {On-line model-checking for finite linear temporal logic specifications},
BookTitle = {Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France},
Volume = {407},
Pages = {275--285},
Series = {LNCS},
Publisher = {Springer-Verlag},
Month = {June},
Year = {1989}
}
Get EndNote Reference (.ref)