Compositional Verification for Timed Systems Based on Automatic Invariant Generation

TL;DR

This paper introduces a compositional verification method for timed systems that automatically generates invariants using auxiliary clocks, effectively managing the state space explosion problem in model-checking.

Contribution

It presents a novel approach combining auxiliary clocks and invariant generation for scalable verification of timed systems with multiple components.

Findings

Successfully implemented in RTD-Finder tool.

Effective in deriving global timing constraints from component timings.

Validated on multiple benchmark examples.

Abstract

We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the timings in the components alone. To this end, we make use of auxiliary clocks to automatically generate new invariants which capture the constraints induced by the synchronisations between components. The method has been implemented in the RTD-Finder tool and successfully experimented on several benchmarks.