Computer Sciences Department

University of Texas at Austin

Austin Tx 78712 USA

emerson@cs.utexas.edu

+1-512-471-9537 (phone)

+1-512-471-8885 (fax)

Abstract: Model checking is an automatic method for verifying correctness of (finite state) reactive programs with respect to temporal logic specifications. The method is algorithmic, exploiting the fixpoint characterizations of the temporal operators to permit a systematic and efficient search of the system state graph. A resulting advantage is that not only does it cater for verification of correctness, but also debugging of incorrect programs through a counter-example facility that program developers find useful. The primary limitation to model checking is the state explosion problem; a related limitation is that the basic method is only applicable to finite state programs.

In this tutorial, we will introduce the basics of temporal logic, its use in describing correctness properties, and the ideas underlying efficient model checking algorithms. We overview the most promising methods for ameliorating state explosion, and techniques for handling classes of infinite state and parameterized systems. We then discuss the role of model checking industry, describing the use of model checking tools for such applications as hardware verification and protocol validation.

Objective: The participant will learn the core theory underlying model checking and gain a good idea as to its domain of applicability.

* Reactive Systems - concurrency, ongoing behavior, etc.

* Temporal Logics

- linear time: PLTL

- Branching time: CTL; CTL*; Mu-calculus

- SnS and automata on infinite objects.

* Expressiveness overview

* Example specifications - safety;liveness; fairness; etc.

* Model checking CTL, Mu-calculus - via Tarski-Knaster theorem

* Model checking PLTL, CTL* - via omega-string automata nonemptiness

or Tarski-Knaster theorem

* Limiting state explosion

- Abstraction: simulation, bisimulations, symmetry reductions, ... etc.

- Partial Order Reduction

- BDDs

- Symbolic Model Checking

- Parameterized and infinite state systems

* Applications

- Industrial goals - verification vs. debugging, etc.

- Implementations and Tools

- Sucesses

- Limitations and Failures

* The Future

Qualifications. Model checking goes back to my dissertation work [Em81](cf. [CE81], [QS82], [CES86]). My work also introduced the CTL branching time logic which is widely used in industry with verification tools such as SMV, VIS, and IBM's RuleBase. The use of the Mu-calculus as a uniform formalism subsuming most commonly used temporal or modal logics of programs was proposed in [EL86], along with polynomial time model checking algorithms for useful fragments of the Mu-calculus. Nowadays much of my time and energy is devoted to methods for overcoming state explosion. I have authored or coauthored a number of research papers on these topics; I have also written various expository papers including "Temporal and Modal Logic" for the Handbook of Theoretical Computer Science; and "Model checking and the Mu-calculus" corresponding to an invited lecture at the DIMACS Symposium on Descriptive Complexity and Finite Models, directed towards an audience of logicians who were not verification experts.

I gave a more specialized invited tutorial on "Mu-calculus Model Checking" at CAV95. Etc. I serve on the editorial boards for Formal Aspects of Computing and Formal Methods in System Design, and am presently Bruton Centennial Professor of Computer Sciences at The University of Texas at Austin.

[CE81] E. M. Clarke and E. A. Emerson, "The Design and Synthesis of Synchronization Skeletons Using Temporal Logic", in Proceedings of the Workshop on Logics of Programs, IBM Watson Research Center, Yorktown Heights, New York, Springer-Verlag Lecture Notes in Computer Science #131, pp. 52-71, 1981.

[CES86] E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic Verificationof Finite State Concurrent Programs using Temporal Logic Specifications", ACM Transactions on Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.

[Em81] E. A. Emerson, "Branching Time Temporal Logic and the Design of Correct Concurrent Programs", Ph.D. Dissertaton, Division of Applied Sciences, Harvard University, 1981.

[EL86] E. A. Emerson and C.-L. Lei, "Efficient Model Checking in Fragments of the Propositional Mu-Calculus", Proceedings of the IEEE-CS Conference on Logic in Computer Science, Cambridge, Massachusetts, pp. 267-278, 1986.

[QS82] J. P. Queille and J. Sifakis, "Specification and Verification of Concurrent Programs in CESAR", Proc. 5th Int. Symp. Prog., Springer LNCS no. 137, pp. 195-220, 1982.