Activity-Based Abstraction Refinement for Timed Systems
Title | Activity-Based Abstraction Refinement for Timed Systems |
Publication Type | Conference Paper |
Year of Publication | 2017 |
Authors | Farkas, R., and Hajdu, Á. |
Conference Name | Proceedings of the 24th PhD Mini-Symposium |
Publisher | Budapest University of Technology and Economics, Department of Measurement and Information Systems |
ISBN Number | 978-963-313-243-2 |
Abstract | Formal analysis of real time systems is important as they are widely used in safety critical domains. Such systems combine discrete behaviours represented by control states and timed behaviours represented by clock variables. The counterexample-guided abstraction refinement (CEGAR) algorithm utilizes the fundamental technique of abstraction to system verification. We propose a CEGAR-based algorithm for reachability analysis of timed systems. The algorithm is specialized to handle the time related behaviours efficiently by introducing a refinement technique tailored specially to clock variables. The performance of the presented algorithm is demonstrated by runtime measurements on models commonly used for benchmarking such algorithms. |
DOI | 10.5281/zenodo.291891 |
PDF: