Timed Automata Verification via IC3 with Zones

摘要

Timed automata are a formal method for the modelling of real-time systems. With a large number of sophisticated tools, ample support for not only specification but also verification is available today. However, although all these tools are highly optimized, verification of timed automata, in particular networks of timed automata, remains challenging. This is due to the large amount of memory needed for storing automata states. In this paper, we present a new approach to timed automata verification based on the SAT-based induction method IC3. Unlike previous work on extending IC3 to timed systems, we employ zones, not regions, for the symbolic representation of timed automata states. While this complicates a timed IC3 procedure, specifically, necessitates the computation of a zone from possibly infinitely many counterexamples to induction, it pays off with respect to memory consumption. Experimental results show that our approach can outperform Uppaal for networks with large numbers of timed automata.