Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems.
Abstract
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(exp 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 better understanding of the behavior of the system, in addition to verifying if its timing requirements are satisfied. We integrate these ideas into the Verus tool, currently under development. To demonstrate how our technique works, we have verified a robotics control system. The results obtained demonstrate that our method can be successfully applied in the analysis of real-time system designs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 12, 1996
- Accession Number
- ADA314486
Entities
People
- E. Clarke
- M. Minea
- S. Campos
- W. Marrero
Organizations
- Carnegie Mellon University