Formal verification of timed systems: a survey and perspective

Wang F.

An overview of the current state of the art of formal verification of real-time systems is presented. We discuss commonly accepted models, specification languages, verification frameworks, state-space representation schemes, state-space construction procedures,eduction techniques, pioneering tools, and finally some new related issues. We also make a few comments according to our experience with verification tool design and implementation.

---

Table of contents :
I. I NTRODUCTION……Page 1
Linear-Time Temporal Logics: The research on automatic verificat……Page 2
Integration of Linear Time and Branching Time: Emerson and Halpe……Page 3
A. Timed Automata……Page 4
B. Communicating Timed Automata……Page 5
E. Timed Process Algebras……Page 6
A. Satisfiability Checking……Page 7
B. Model Checking……Page 8
D. Theorem Proving……Page 9
B. BDD-Like Data Structures……Page 10
VI. C ONSTRUCTION OF T IME -S PACE R EPRESENTATIONS……Page 11
C. On-the-Fly Approach……Page 12
E. Approximation……Page 13
F. PARAGON……Page 14
L. RED……Page 15
C. Controller Synthesis……Page 16
X. S UMMARY AND P ERSPECTIVES……Page 17
J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi, U……Page 18
E. A. Emerson and A. P. Sistla, Utilizing symmetry when model-ch……Page 19
R. M. Karp and R. E. Miller, Parallel program schemata, J. Compu……Page 20
J. S. Ostroff, Temporal Logic of Real-Time Systems, ser. Advance……Page 21
F. Wang, G.-D. Hwang, and F. Yu, Symbolic simulation of industri……Page 22
L. Zhang, C. Madigan, M. Moskewicz, and S. Malik, Efficient conf……Page 23