KEYS IN FORMAL VERIFICATION

摘要

These lecture notes present a set of techniques for the verification of reactive systems. We concentrate on the case of infinite-states systems and the application of abstraction methods for their verification. After introducing the computational model of fair discrete systems (FDS) and the specification language of (linear) temporal logic (TL), we describe a standard approach to verification by Finitary abstraction. This is a method by which an infinite-state system is abstracted into a finite-state system which can then be model checked. We begin by providing a general sound recipe for the finitary abstraction of a verification problem which jointly abstracts the system and its temporal specification. We show that predicate abstraction is a special case of this sound recipe. We then show that state abstraction is not adequate for proving liveness properties by abstraction. We introduce the method of augmented finitary abstraction by which, the system is augmented by a progress monitor prior to its abstraction. It is claimed that this extended method is complete for proving by abstraction any temporal property of an infinite-state systems. We show that augmented abstraction is a practical approach to proofs of live-ness properties, and is simpler to apply than corresponding deductive proofs which require the design of a full ranking function which decreases on every helpful step. We illustrate the power of the programmable model checker TLV and demonstrate how it can be used for the automatic computation of abstracted systems. This includes an example of shape analysis by predicate abstraction.