Temporal Verification of Real-Time Systems

Sérgio V. CAMPOS  Edmund M. CLARKE  Wilfredo MARRERO  Marius MINEA  Hiromi HIRAISHI  

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E78-D   No.7   pp.796-801
Publication Date: 1995/07/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Issue on Verification, Test and Diagnosis of VLSI Systems)
Category: 
Keyword: 
formal verification,  real-time system,  temporal logic,  

Full Text: PDF(633KB)
>>Buy this Article


Summary: 
This paper presents 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 a 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. The algorithms presented in this paper are efficiently implemented using binary decision diagrams and have been incorporated into the SMV symbolic model checker. Using this method, we have verified a model of an aircraft control system with 1015 states. The results obtained demonstrate that our method can be successfully applied in the verification of real-time system designs.