Accession Number:

ADA282839

Title:

Computing Quantitative Characteristics of Finite-State Real-Time Systems

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Report Date:

1994-05-04

Pagination or Media Count:

24.0

Abstract:

Current methods for verifying real-time systems are essentially decision procedures that establish whether the system model satisfies a given specification. We present a general method for computing quantitative information about finite-state real-time systems. We have developed algorithms that compute exact bounds on the delay between two specified events and on the number of occurrences of an event in at given interval. 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 system behavior, in addition to determining its correctness. We also show that our technique can be extended to a more general representation of real-time systems, namely, timed transition graphs. The algorithms presented in this paper have been incorporated into the SMV model checker and used to verify a model of an aircraft control system. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs

Subject Categories:

  • Aircraft
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE