Accession Number : ADA328565


Title :   Temporal Specification and Verification of Real-Time Systems.


Descriptive Note : Doctoral theses,


Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE


Personal Author(s) : Henzinger, Thomas A.


Full Text : http://www.dtic.mil/dtic/tr/fulltext/u2/a328565.pdf


Report Date : 30 AUG 1991


Pagination or Media Count : 295


Abstract : We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of reactive systems. Semantics: We introduce the abstract computational model of timed transition systems as a conservative extension of traditional transition systems: qualitative fairness requirements are superseded by quantitative real-time constraints on the transitions. Digital clocks are introduced as observers of continuous real-time behavior. We justify our semantical abstractions by demonstrating that a wide variety of concrete real-time systems can be modeled adequately. Specification: We present two conservative extensions of temporal logic that allow for the specification of timing constraints: while timed temporal logic provides access to time through a novel kind of time quantifier, metric temporal logic refers to time through time-bounded versions of the temporal operators. We justify our choice of specification languages by developing a general framework for the classification of real-time logics according to their complexity and expressive power. Verification: We develop tools for determining if a real-time system that is modeled as a timed transition system meets a specification that is given in timed temporal logic or in metric temporal logic. We present both model-checking algorithms for the automatic verification of finite-state real-time systems and proof methods for the deductive verification of real-time systems.


Descriptors :   *SOFTWARE ENGINEERING , *REAL TIME , *COMPUTER PROGRAM VERIFICATION , MATHEMATICAL MODELS , ALGORITHMS , DATA MANAGEMENT , COMPUTER COMMUNICATIONS , SPECIFICATIONS , COMPUTER LOGIC , SEMANTICS , SYSTEMS ANALYSIS , SYNTAX , MULTIPROGRAMMING.


Subject Categories : COMPUTER PROGRAMMING AND SOFTWARE
      COMPUTER SYSTEMS


Distribution Statement : APPROVED FOR PUBLIC RELEASE