Automated Logical Verification based on Trace Abstractions

Abstract

We propose a new and practical framework for integrating the behavioral
reasoning about distributed systems with model-checking methods.
Our proof methods are based on trace abstractions, which relate the
behaviors of the program and the specification. We show that for finite-state
systems such symbolic abstractions can be specified conveniently in
Monadic Second-Order Logic (M2L). Model-checking is then made possible
by the reduction of non-determinism implied by the trace abstraction.
Our method has been applied to a recent verification problem by Broy
and Lamport. We have transcribed their behavioral description of a distributed
program into temporal logic and verified it against another distributed
system without constructing the global program state space. The
reasoning is expressed entirely within M2L and is carried out by a decision
procedure. Thus M2L is a practical vehicle for handling complex temporal
logic specifications, where formulas decided by a push of a button are as
long as 10-15 pages.