Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems

Symbolic model checking is a technique for verifying finite-state concurrent systems that has been extended to handle real-time systems. Models with up to 10 30 states can often be verified in minutes. In this paper, we present a new tool to analyze real-time systems, based on this technique. We have designed a language, called Verus, for the description of real-time systems. Such a description is compiled into a state-transition graph and represented symbolically using binary decision diagrams. We have developed new algorithms for exploring the state space and computing quantitative information about the system. In addition to determining the exact bounds on the delay between two specified events, we compute the number of occurrences of an event in all such intervals. This technique allows us to determine performance measures such as schedulability, response time, and system load. Our algorithms produce more detailed information than traditional methods. This information leads to a ..