Refining Model Checking by Abstract Interpretation

Patrick COUSOT

Abstract

Formal methods combining abstract interpretation and model-checking have been considered to cope with the high complexity of very large systems and the undecidability problems for infinite state systems. Consequently, all properties of all systems cannot be automatically verified in finite or reasonable time. Some form of approximation has to be considered.

In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/$\mu$-calculus model-checking can be directly applied.

Two improvements of abstract model-checking are proposed which can be applied to infinite abstract transition systems:

A new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction;
When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyses for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking.

Lucidi

Reference:

P. Cousot and R. Cousot.
``Refining Model Checking by Abstract Interpretation'',
In: Automated Software Engineering, 6(1), 1999, to appear.

Surveys on model checking:

E.M.Clarke, O. Grumberg, D.E. Long:
`` Verification Tools for Finite-State Concurrent Systems'',
LNCS 803, in the proceedings of REX school/symposium on A decade of concurrency: reflections and perspectives,
Noordwijkerhout, The Netherlands, June 1993.
E.M.Clarke, O. Grumberg, D.E. Long:
`` Model Checking'', in Springer-Verlag Nato ASI Series F, Volume 152, 1996 (a survey on model checking, abstraction and composition).