«TECHNIQUES FOR AUTOMATIC VERIFICATION OF REAL-TIME SYSTEMS a dissertation submitted to the department of computer science and the committee on ...»
TECHNIQUES FOR AUTOMATIC VERIFICATION OF
submitted to the department of computer science
and the committee on graduate studies
of stanford university
in partial fulfillment of the requirements
for the degree of
doctor of philosophy
c Copyright 1991 by Rajeev Alur
All Rights Reserved
I certify that I have read this dissertation and that in my
opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.
David Dill (Principal Advisor) I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.
Zohar Manna (Coadvisor) I certify that I have read this dissertation and that in my opinion it is fully adequate, in scope and in quality, as a dissertation for the degree of Doctor of Philosophy.
Approved for the University Committee on Graduate Studies:
Dean of Graduate Studies iii Abstract This thesis proposes formal methods for speci cation and automatic veri cation of nitestate real-time systems. The traditional formalisms for reasoning about programs abstract away from quantitative time and, consequently, are inadequate for reasoning about realtime systems. We extend the methods based on automata and temporal logics to allow them to model timing delays and to verify real-time requirements.
We introduce timed automata to model the behavior of real-time systems over time.
Our de nition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using nitely many real-valued clocks. A timed automaton accepts timed words | strings in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses.
We present two conservative extensions of the existing temporal logics to allow them to specify timing properties. The metric interval temporal logic (MITL) uses linear-time semantics, and its syntax allows temporal operators to be subscripted with intervals restricting their scope in time. The timed computation tree logic (TCTL) uses branching-time semantics, and its syntax provides access to time through a novel kind of time quanti er.
In the proposed veri cation method, a nite-state system is modeled as a composition of timed automata, and the correctness is speci ed either as a deterministic timed automaton, or as a formula of MITL or TCTL. In each case we develop an algorithm for model checking. The distinguishing feature of our work is the use of the set of reals to model time we argue that the denseness of the time domain is crucial for modeling event-driven asynchronous systems. The thesis also clari es the relationship between di erent models and logics for real-time, and answers some basic questions regarding complexity, decidability, and expressiveness.
iv Acknowledgments First of all I thank my advisors, David Dill and Zohar Manna, for o ering me technical, nancial, and moral support during the last four years. My reading committee comprised of David, Zohar, and Moshe Vardi, and I consider myself fortunate that I had access to valuable guidance from all three of them. I am also thankful to them for their critical reading of the draft. Zohar introduced me to temporal logics, and directed me to the relatively unexplored area of real-time logics. He also made possible an extremely productive visit to the Weizmann Institute in Israel. Much of the research reported in this thesis is inspired by my discussions with David about his ideas on coupling automata with timing constraints.
Moshe is one of the leading proponents of the automata-theoretic approach to veri cation, and his expertise on the subject has been very useful to me.
It has been a great pleasure for me to work closely with Tom Henzinger. We learned to do research together we solved many problems together it would be futile to pinpoint his
innumerable contributions towards my work. Special thanks also go to my other colleagues:
Costas Courcoubetis and Tomas Feder. Costas's unbounded enthusiasm to attack new problems has been a source of inspiration to me. The decision procedure for MITL builds upon some insightful observations made by Tomas.
I have had the opportunity to discuss my research with many scientists at Stanford, at IBM Almaden Research Center, and at various conferences and seminars. I thank all of them for being helpful and encouraging. I am particularly grateful to Joe Halpern, Dinesh Katiyar, John Mitchell, Amir Pnueli, Howard Wong-Toi, and Mihalis Yannakakis.
My allegiance to computer science is mainly due to the excellent education I received at the Indian Institute of Technology at Kanpur, and I am thankful to the faculty on its Computer Science Department. Also this thesis would not exist without the love and support of my family, especially, my parents. I would also like to use this opportunity to thank all my friends on Stanford campus because of them my stay here has been very enjoyable and memorable.
1.1 Motivation With the increasing use of computers in safety-critical applications there is a pressing need for designing more reliable systems. As a result, developing formal methods for the design and analysis of concurrent systems has been an active area of computer science research. The conventional approach to testing the correctness of a system involves simulation on some test cases. This method is quite inadequate for developing bug-free complex concurrent systems. One approach to assure correctness is to employ automatic veri cation methods.
A veri cation formalism comprises of
1. A formal semantics which assigns mathematical meanings to system components and correctness criteria.
2. A language for describing the essential aspects of the system components, and constructs for combining them.
3. A speci cation language for expressing the correctness requirements.
4. A veri cation algorithm to check if the correctness criteria are ful lled in every possible execution of the system.
In this thesis we provide formalisms for automatic veri cation of nite-state real-time systems.
The class of systems to which our methods are applicable includes asynchronous circuits, communication protocols, and controllers (such as a ight controller, or a controller for a
CHAPTER 1. INTRODUCTION 2
manufacturing plant). The essential characteristics of such systems are:
Finite-state: The system can be in one of the nitely many discrete states. If we focus only on the control aspect of the system, ignoring the computational aspect, then this is an useful abstraction in many cases. State-transitions are triggered by events which are instantaneous.
Reactive: The system constantly interacts with the environment reacting to stimuli.
So we are interested in the ongoing behavior over time. This is quite unlike the traditional \transformational" view of the programs where the functional relationship between the input state and the output state de nes the meaning of a program. The system comprises of a collection of components operating concurrently and communicating with each other.
Real-time: The correctness of the system depends on the actual magnitudes of the timing delays of the components. This is obviously the case when the system needs to meet hard real-time deadlines: the system needs to respond to a stimulus within a certain xed time bound. Also there are cases when the logical correctness of the system depends on the lengths of various delays.
Real-time systems are used in safety-critical applications such as controllers for nuclear plants. Failures in such systems can be very expensive and even life-threatening. Because of the intricacies of the timing relationships, real-time systems are quite hard to model, specify, and design. Consequently, there is a great demand for formal methods applicable to real-time systems.
1.2 Background: formalisms for qualitative reasoning Several di erent formalisms have been proposed to reason about reactive systems. These include Petri nets, process algebras, temporal logics, automata-theoretic techniques, and partial-order models.
from time, retaining the information about the causality and/or the temporal order of occurrence of observable events. Even though there is no general agreement about what is the right semantics of concurrency, some of these techniques have provided the foundations for building veri ers for hardware and communication protocols, and some have suggested structured disciplines for writing concurrent programs. We
CHAPTER 1. INTRODUCTION 3will brie y review these approaches the methods for automatic veri cation of nite-state systems are of main interest to us.
1.2.1 Temporal logics The use of temporal logic as a formalism for specifying the behavior of a reactive system over time was rst proposed by Pnueli in 1977 Pnu77]. The subject has been extensively studied since then BMP81, MP81, EC82, OL82, Lam83, MW84, BKP86, CES86, Pnu86, MP89, Lam91]. Temporal logic is a modal logic with modalities such as 3 meaning \eventually", and 2 meaning \always" (see Eme90] for an overview). Temporal logics provide a succinct and natural way of expressing the desired temporal requirements. Two types of temporal logics have been proposed: linear-time and branching-time.
In the linear-time framework, a system is viewed as a set of computations, where each computation is a sequence of system-states recording all the transitions over the course of time. A linear temporal logic formula is interpreted over such state sequences Pnu77, OL82]. The branching-time logics, on the other hand, are interpreted over tree models BMP81, EC82, EL85]. The system is viewed as a nitely-branching tree the paths in the tree correspond to the possible executions of the system.
In the traditional approach to veri cation of concurrent programs, the correctness of the program is expressed by a formula in rst-order temporal logic. The veri cation problem reduces to proving a theorem in a deductive system. For example, Manna and Pnueli MP89] have developed the model of fair transition systems to describe the implementation, and give a proof system to verify temporal logic speci cations. Though the technique is quite general, constructing a proof needs to be done manually and requires a great deal of understanding of the program. The only extent of automation one can hope for is to have the proof checked by a machine and possibly to have some limited heuristics in nding the proof.
Model checking provides a di erent approach to checking properties of nite-state systems CES86, LP85, EL85, BCD+ 90, GW91]. In this approach, the global state-transition graph is viewed as a nite Kripke structure (with fairness requirements, if necessary). The speci cation of the system is given as a formula of a propositional temporal logic. The model-checking algorithm then decides whether the system meets the speci cation in all possible scenarios. For the linear-time case, the complexity of model-checking is linear in the size of the state-transition graph and exponential in the size of the speci cation, and in
CHAPTER 1. INTRODUCTION 4the branching-time case, it is linear both in the size of the state-transition graph and the length of the temporal logic speci cation. Various aspects of the model-checking problem for the logic CTL EC82] have been studied. This approach has been successfully applied to verify circuits and protocols, and to nd bugs in previously-published, non-trivial protocols and circuits CES86, BCDM86].
The model-checking approach to program veri cation is probably the most exciting advance in the theory of program correctness in recent years. It has been extended to probabilistic systems Var85, PZ86, CY88], to real-time systems EMSS89, AH89, ACD90, Lew90, HLP90], and to probabilistic real-time systems HJ89, ACD91a, ACD91b].
The main di culty in using model-checking approach is the state-explosion problem: the size of the global state-transition graph grows exponentially with the number of components in the system. This problem has received great attention recently, and di erent ways to cope with the problem have been proposed BCD+ 90, God90, GW91].
1.2.2 Automata-theoretic approach A related approach to veri cation of nite-state systems uses !-automata WVS83, Var87].
The computation of a reactive program is viewed as an in nite word over the alphabet of events (or states). This gives rise to an intimate connection between reasoning about reactive systems and the formal language theory. A system is modeled as an automaton generating in nite sequences which correspond to the possible computations of the system.
The automata over in nite words were rst studied by Buchi in relation to the theory S1S, the second order monadic theory of natural numbers with successor Buc62]. Buchi automata and their variants have been studied in great detail since then Cho74, Mul63, McN66], leading to a beautiful theory of !-regular languages (see Tho90] for an overview).
In the automata-theoretic framework, a system is modeled as a composition of several automata. The implementation automaton I is the product of these automata, and acts as a generator. The speci cation is given as another automaton S which acts as an acceptor. Alternatively, from a linear temporal logic speci cation, one can construct an automaton which accepts all the computations that satisfy the given formula. The implementation is correct i every behavior generated by I is accepted by S. Thus the veri cation problem reduces to the language inclusion problem. Consequently the known e ective constructions for intersection, complementation, and test for emptiness can be used