Automated Invariant Generation for the Verification of Real-Time Systems

We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We first introduce the CIPM algorithm which computes new invariants for timed automata control locations taking their originally defined invariants as well as the constraints imposed by incoming state transitions into account. CIPM also prunes transitions that can never be taken from the automaton. We then compute a predicate abstraction taking information regarding control locations and their newly computed invariants into account. We finally discuss a prototype implementation of our technique