Techniques for automatic verification of real-time systems

Abstract

This thesis proposes formal methods for specification and automatic verification of finite-state real-time systems. The traditional formalisms for reasoning about programs abstract away from quantitative time and, consequently, are inadequate for reasoning about real-time 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 definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. 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 quantifier. In the proposed verification method, a finite-state system is modeled as a composition of timed automata, and the correctness is specified 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 clarifies the relationship between different models and logics for real-time, and answers some basic questions regarding complexity, decidability, and expressiveness.