Accession Number:

ADA314486

Title:

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

Descriptive Note:

Research rept.,

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Report Date:

1996-08-12

Pagination or Media Count:

13.0

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 10exp 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.

Subject Categories:

  • Computer Programming and Software
  • Cybernetics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE