A Quantitative Approach to the Formal Verification of Real-Time Systems

Abstract The task of checking if a computer system satisfies its timing specifications is extremelyimportant. These systems are often used in critical applications where failure to meet a deadline can have serious or even fatal consequences. This work proposes an efficientmethod for performing this verification task. The method is based on temporal logic model checking, a technique for verifying concurrent reactive systems. In the proposedtechnique, a real-time system is modeled by a state-transition graph represented by binary decision diagrams. Efficient symbolic algorithms exhaustively explore the state space todetermine whether the system satisfies a given specification