# 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

- J Strother Moore, Supervisor
- Lorenzo Alvisi
- E. Allen Emerson
- Matt Kaufmann
- Jayadev Misra
- Amir Pnueli

Gzipped Postscript (307K)

PDF (682K)

Postscript (886K)