Symbolic verification with gap-order constraints
Finite state automata with counters are useful for modelling systems with discrete parameters. The calculation of state invariants is an important tool in the analysis of such systems. Previous authors have presented techniques for the calculation of state invariants based on their approximation by convex polyhedra or periodic sets.
In this paper we present a new method for the calculation of invariants for finite state automata with counters, based on their representation by gap-order constraints. This method differs from previous approaches by exploiting existing techniques for the calculation of least fixed points. The use of least fixed points reduces the need for approximation and allows the generation of non-convex invariants. We do not need to specify the initial inputs to the automaton, but can leave them as uninstantiated parameters, or partially specify them using gap-order constraints. Our method not only provides a new tool for program analysis, but is also an interesting application of logic programming techniques.
KeywordsState Invariant Internal Transition Convex Polyhedron External Transition Finite State Automaton
Unable to display preview. Download preview PDF.
- 1.R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In Proceedings of 5th IEEE LICS, pages 414–425. IEEE, 1990.Google Scholar
- 2.B. Boigelot and P. Wolper. Symbolic verification with periodic sets. In Proceedings of conference on Computer-Aided Verification, 1994, pages 55–67, 1994.Google Scholar
- 3.L. Fribourg and H. Olsén. Datalog programs with arithmetical constraints: hierarchic, periodic and spiralling least fixed points. Research report 95-26, Laboratoire Informatique, École Normale Supérieure, Paris, November 1995.Google Scholar
- 4.L. Fribourg and J. D. C. Richardson. Symbolic verification with gap-order constraints. Report LIENS — 96 — 3, Laboratoire d'Informatique, École Normale Supérieure (LIENS), Paris, February 1996. Available by ftp from host ftp.ens.fr in directory /pub/reports/liens.Google Scholar
- 5.L. Fribourg and M. Veloso Peixoto. Bottom-up evaluation of Datalog programs with arithmetic constraints. In Alan Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 814, pages 311–325, Nancy, France, 1994. Springer-Verlag.Google Scholar
- 6.N. Halbwachs. Delay analysis in synchronous programs. In Proceedings of conference on Computer-Aided Verification, 1993, pages 333–346, 1993.Google Scholar
- 7.T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings 7th LICS Symposium, Santa Cruz, pages 394–406, 1992.Google Scholar
- 8.A. Kerbrat. Méthodes Symboliques pour la Vérification des Processus Communicants: étude et mise en oeuvre. PhD thesis, L'Université Joseph Fourier — Grenoble I, November 1994. In French.Google Scholar
- 9.A. Kerbrat. Reachable state space analysis of LOTOS specifications. In Proceedings of the 7th international conference on formal description techniques, pages 161–176, 1994.Google Scholar