Automatic Methods and Tools for the Verification of Real Time Systems

摘要

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 lan(caret)maage 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.