Mechanical Verification of Reactive Systems

Panagiotis Manolios.
Presented to the faculty of the Graduate School of the University of Texas at Austin in August 2001.

Abstract

It is increasingly crucial to the well-being of our society that safety-critical computing systems behave correctly. Examples of such systems include air traffic control systems, medical monitoring systems, systems for controlling nuclear reactors, communication protocols, and microprocessors. All of the above are examples of reactive systems, non-terminating computing systems that maintain an ongoing interaction with their environment. Establishing correctness requires proof. However, due to the complexity of reactive systems, hand proofs are not reliable: just the description of a system can be hundreds of pages long! The only viable solution is mechanical verification, where a computer program is employed to check and to help construct proofs of correctness. The main obstacle to the widespread use of mechanical verification is that it requires considerable human effort. In this dissertation, we show how to reduce the effort involved in the mechanical verification of reactive systems.

We start by considering notions of correctness that allow us to relate a reactive system to a simpler system that acts as the specification. Notions of correctness for reactive systems characterize the relationship between infinite computations of the implementation and of the specification. To simplify the effort involved in reasoning mechanically about such notions, we develop a compositional theory of refinement with proof rules that are based on reasoning about single steps of reactive systems, as opposed to infinite computations, which is otherwise required.

In the next part of the dissertation, we present a novel approach to combining theorem proving and model checking, the two leading mechanical verification paradigms. Theorem proving is very general, but requires considerable human interaction; model checking does not require human reasoning, but is only applicable to ``small'' systems. With our approach, theorem proving is employed to prove the correctness of an abstraction that yields a reduced system. We introduce algorithms for extracting reduced systems which are then analyzed using model checking. This is a very general abstraction technique that allows great flexibility in choosing an appropriate abstraction. The general idea is to reduce the problem to one that can be model checked in a reasonable amount of time. We use the ACL2 (A Computational Logic for Applicative Common Lisp) theorem proving system to implement the ideas, e.g., we develop and verify a model checker for the Mu-Calculus using ACL2.

The dissertation concludes with two case studies. The first case study concerns the verification of a simple {communications protocol. This case study highlights the use of our extraction algorithm and our approach to combining theorem proving and model checking. The second case study involves the verification of a simple pipelined machine from the literature. We show that the notion of correctness we use more faithfully represents the informal correctness requirements than other notions of correctness currently in use. In addition, we show that it is possible to automate much of the verification effort in ACL2 by using libraries of general purpose theorems. Finally, we verify several variants of the pipelined machine including machines with exceptions, interrupts, and netlist (gate-level) descriptions.

Committee

Gzipped Postscript (307K)
PDF (682K)
Postscript (886K)