Efficient Verification of Timed Automata

Advisors : F. Herbreteau, and I. Walukiewicz
Institution : Laboratoire Bordelais de Recherche en Informatique (LaBRI)
Team : Formal Methods, Modelling and Verification group

Keywords

Timed automata, Model-checking, Abstraction, Real-time Systems.

Description

Timed automata[1] are finite automata extended with clocks that can be reset and tested on the transitions. Clocks allow to contrain the delay between actions of the automaton. Timed automata are widely used to model real-time systems and for model-checking real-time specifications.

The state-space of a timed automaton is infinite (and even not countable). To overcome this problem, verification algorithms use a finite abstraction of the runs of the automaton[2]. The efficiency of the verification algorithms heavily rely on the coarseness of the abstraction[3].

These last years, several optimizations of the abstractions and the underlying algorithms have been proposed[4,5,6,7,8,9]. In particular, new properties of convex sets of clock values have been established. This allowed to obtain a new algorithm for handling abstractions of such convex sets. The algorithm opens many new possibilties in algorithmics of reachability testing, with an expected gain of several order of magnitude with respect to the existing approaches. The subject is quite large and permits for both purely theoretical and implementation contributions depending on the interests of the student.

Some first possible goals are:

Bibliography