Fast On-the-Fly Parametric Real-Time Model Checking

12 years 3 months ago
Fast On-the-Fly Parametric Real-Time Model Checking
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 errordetection 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.
Dezhuang Zhang, Rance Cleaveland
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where RTSS
Authors Dezhuang Zhang, Rance Cleaveland
Comments (0)