loading...
Fast On-the-Fly Parametric Real-Time Model Checking
Miami, Florida December 05-December 08
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/RTSS.2005.2226th IEEE International Real-Time Sys ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Dezhuang Zhang, State University of New York at Stony Brook
Rance Cleaveland, University of Maryland at College Park
This paper presents a local algorithm for solving the universal parametric real-time model-checking problem. The problem may be phrased as follows: given a real-time system and temporal formula, both of which may contain parameters, and a constraint over the parameters, does every allowed parameter assignment ensure that the real-time system satisfies the formula? Our approach relies on translating these model-checking problems into predicate equation systems, and then using an efficient proof-search algorithm to solve these systems. Experimental data shows that our method substantially outperforms existing approaches for systems that contain errors, while exhibiting comparable behavior for systems that are correct. This fast error-detection capability of our technique makes it especially interesting for design approaches in which model checkers are used "early and often" to detect design errors in an ongoing manner.
Citation:
Dezhuang Zhang, Rance Cleaveland, "Fast On-the-Fly Parametric Real-Time Model Checking," rtss, pp.157-166, 26th IEEE International Real-Time Systems Symposium (RTSS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.