Combining dynamic algorithms for timed automata verification

Keywords

Model-checking, Timed automata, Abstract zone graph, Dynamic abstraction, State-space exploration strategy, Partial-order techniques

Advisor

F. Herbreteau

Abstract

Timed automata (AD94) is a widely accepted model for real-time system verification. Formal verification algorithms usually perform a state-space exploration of the automaton to ensure that a given specification is satisfied. The state-space of a timed automaton is uncountable. Hence, algorithms rely on finite abstractions that faithfully represent the state-space of the automaton. Alur and Dill introduced the region graph abstraction in (AD94), however this approach does not scale beyond very simple timed automata. Several abstractions have been introduced based on zone graphs that allowed scale formal verification to timed automata modeling industrial case studies (DT98, BBFL03, BBLP06, HSW16, GHSW19). In parallel, several optimisations of the state-space exploration algorithms have been proposed (DT98, HSW13, HT15, RSM19).

The goal of this internship is to combine several of the optimisations above in a new algorithm that improves state-of-the-art approaches. We particularly focus on the following techniques:

Combining these three techniques is far from obvious as, for instance, some of them rely on incompatible exploration strategies of the state-space. The goal of this internship is to study the core ideas behind these techniques and to propose a new algorithm that benefit from them. The new algorithm will be implemented in the tool TChecker (TCK) and evaluated on standard benchmarks from the litterature.