DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
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
Report Date:
1996-09-01
Pagination or Media Count:
212.0
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.
Distribution Statement:
APPROVED FOR PUBLIC RELEASE
