Activity-Based Abstraction Refinement for Timed Systems

CímActivity-Based Abstraction Refinement for Timed Systems
Közlemény típusaConference Paper
Kiadás éve2017
SzerzőkFarkas, R., and Hajdu, Á.
Konferencia neveProceedings of the 24th PhD Mini-Symposium
KiadóBudapest University of Technology and Economics, Department of Measurement and Information Systems

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.