Accession Number : ADA326972
Title : A Quantitative Approach to the Formal Verification of Real-Time Systems.
Descriptive Note : Doctoral thesis,
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Campos, Sergio V.
PDF Url : ADA326972
Report Date : SEP 1996
Pagination or Media Count : 212
Abstract : The task of checking if a computer system satisfies its timing specifications is extremely important. These systems are often used in critical applications where failure to meet a deadline can have serious or even fatal consequences. This work proposes an efficient method for performing this verification task. The method is based on temporal logic model checking, a technique for verifying concurrent reactive systems. In the proposed technique, a real-time system is modeled by a state-transition graph represented by binary decision diagrams. Efficient symbolic algorithms exhaustively explore the state space to determine whether the system satisfies a given specification. In addition to accepting an explicit timing constraint, and checking if it is satisfied, our approach computes quantitative timing information such as minimum and maximum time delays between given events. These results provide insight into the behavior of the system as well as assist in the determination of its temporal correctness. The technique evaluates how well the system works or how seriously it fails, as opposed to only if it works or not, allowing a much richer analysis than previous methods. Response time to events, schedulability of a task set and system performance are examples of information produced by our algorithms. They also provide insight into how changes in the parameters affect global behavior and allow fine-tuning of the system based on these results.
Descriptors : *CONCURRENT ENGINEERING, *COMPUTER PROGRAM VERIFICATION, ALGORITHMS, COMPUTERIZED SIMULATION, SOFTWARE ENGINEERING, ROBOTICS, OPTIMIZATION, DISTRIBUTED DATA PROCESSING, REAL TIME, COMPUTER LOGIC, SEMANTICS, THESES, MULTIPROCESSORS, SYSTEMS ANALYSIS, CONTROL THEORY, SYNTAX, COMPUTER PROGRAM RELIABILITY.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE