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
Personal Author(s) : Campos, S. ; Clarke, E. ; Marrero, W. ; Minea, M.
PDF Url : ADA314486
Report Date : 12 AUG 1996
Pagination or Media Count : 13
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.
Descriptors : *ROBOTICS, *REAL TIME, *SYMBOLIC PROGRAMMING, ALGORITHMS, OPTIMIZATION, SYSTEMS ENGINEERING, DATA MANAGEMENT, DISTRIBUTED DATA PROCESSING, COMPUTER COMMUNICATIONS, CONCURRENT ENGINEERING, SCHEDULING, SYSTEMS ANALYSIS, CONTROL THEORY, COMPUTER PROGRAM VERIFICATION, COMPILERS, CONTROL SEQUENCES, STRUCTURED PROGRAMMING, AUTOMATIC PROGRAMMING.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE