Automatic Methods and Tools for the Verification of Real Time Systems
Abstract
We developed formal methods and tools for the verification of real-time systems. This was accomplished by extending techniques, based on automata theory and temporal logic, that have been successful for the verification of time-independent reactive systems. As system specification language for embedded real-time systems, we introduced hybrid automata, which equip traditional discrete automata with real-numbered clock variables and continuous environment variables. As requirements specification languages, we introduced temporal logics with clock variables for expressing timing constraints. Since the state spaces of systems with real-numbered clock variables are infinite, all verification must proceed symbolically. Symbolic verification methods are based either on deductive reasoning, using proof rules for symbolic logics, or on algorithmic analysis, using model checking procedures that operate on symbolic representations of state sets. We developed proof calculi for checking if a hybrid automaton satisfies linear-time clock properties, and we developed and implemented symbolic procedures for checking if a piecewise-linear hybrid automaton satisfies branching-time clock properties. The continuous variables of piecewise linear hybrid automata follow trajectories within piecewise-linear envelopes, which can be used to approximate conservatively the behavior of more general, nonlinear systems. We also studied the complexity of various formulations of the verification problem for real-time systems, and we identified the exact boundary between decidability and undecidability of real-time reasoning.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 30, 1997
- Accession Number
- ADA387021
Entities
People
- Thomas A. Henziger
Organizations
- University of California, Berkeley