Report Number: CS-TR-96-1571
Institution: Stanford University, Department of Computer Science
Title: Formal Verification of Performance and Reliability of Real-Time Systems
Author: DeAlfaro, Luca
Date: June 1996
Abstract: In this paper we propose a methodology for the specification and verification of performance and reliability properties of real-time systems within the framework of temporal logic. The methodology is based on the system model of stochastic real-time systems (SRTSs), and on branching-time temporal logics that are extensions of the probabilistic logics pCTL and pCTL*. SRTSs are discrete-time transition systems that can model both probabilistic and nondeterministic behavior. The specification language extends the branching-time logics pCTL and pCTL* by introducing an operator to express bounds on the average time between events. We present model-checking algorithms for the algorithmic verification of system specifications, and we discuss their complexity.