The increased use of real-time systems in critical applications (those with a high failure cost) has intensified the need and desire to verify these systems. The distinguishing feature of real-time systems are the hard timing constraints placed on their execution. Thus, research efforts will be concentrated on the correctness of real-time processes with respect to timing constraints. The two objectives of this research are the development of an algebraic theory for specifying and verifying real-time processes and the implemenation of verification tools based on the algebraic theory developed. The algebraic approach provides a single paradigm for performing both specification and verification. The algebraic specification language contains constructs for representing the temporal and structural properties that arise in real-time processes. The semantics of this language defines an equational logic that can be used to analyze real-time processes. This logic contains rules for reasoning about hard timing constraints. In addition, it provides rules for reasoning about non-temporal properties of real-time processes such as freedom from deadlock and process interaction. A verification tool based on this logic will be implemented using an automatic theorem prover.
