Activity-Based Abstraction Refinement for Timed Systems

TitleActivity-Based Abstraction Refinement for Timed Systems
Publication TypeConference Paper
Year of Publication2017
AuthorsFarkas, R., and Hajdu, Á.
Conference NameProceedings of the 24th PhD Mini-Symposium
PublisherBudapest University of Technology and Economics, Department of Measurement and Information Systems
ISBN Number978-963-313-243-2

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.