TY - CONF
AB - We propose an incremental workflow for the verification of parameterized systems modeled as symmetric networks of timed automata. Starting with a small number of timed automata in the network, a safety property is verified using IC3, a state-of-the-art algorithm based on induction.The result of the verification, an inductive strengthening, is reused proposing a candidate inductive strengthening for a larger network.If the candidate is valid, our main theorem states that the safety property holds for all sizes of the network of timed automata. Otherwise the number of automata is increased and the next iteration is started with a new run of IC3.We propose and thoroughly examine optimizations to our workflow, e.g. Feedback mechanisms to speed up the run of IC3.
AU - Isenberg, Tobias
ID - 285
T2 - Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD)
TI - Incremental Inductive Verification of Parameterized Timed Systems
ER -