Efficient Verification of Timed Automata
Advisors : F. Herbreteau, and I. Walukiewicz
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:
- to develop new abstractions that could dynamically use
the informations that are collected by verification algorithms,
- to study which are the properties preserved by these abstractions
(in particular, regarding probabilistic and quantitative/priced
extensions of timed automata),
- to integrate verification techniques designed for distributed
systems,
- to combine with program verification techniques in order to check
real-time programs.
Bibliography
- [1] R. Alur and D. Dill. A Theory of Timed Automata. Theoretical
Computer Science, 126: 183-235, 1994.
- [2] C. Daws and S. Tripakis. Model checking of real-time reachability
properties using abstractions. Int. Conf. on Tools and Algorithms for
the Construction and Analysis of Systems (TACAS), LNCS vol. 1384,
Springer, 1998.
- [3] G. Behrmann and P. Bouyer and K.G. Larsen and R. Pelanek. Lower
and upper bounds in zone-based abstractions of timed automata. Int. J.
on Software Tools for Technology Transfer (STTT), 8(3): 204-215, 2006.
- [4] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient
Emptiness Check for Timed Büchi Automata. Proc 22nd Int. Conf. on
Computer Aided Verification (CAV), 2010.
- [5] F. Herbreteau and B. Srivathsan. Efficient On-The-Fly Emptiness
Check for Timed Büchi Automata. Proc. 8th Int. Symp. on Automated
Technology for Verification and Analysis (ATVA), 2010.
- [6] F. Herbreteau and B. Srivathsan. Coarse abstractions make Zeno
behaviors difficult to detect. Proc. 22nd Int. Conf. on Concurrency
Theory (CONCUR), 2011.
- [7] F. Herbreteau, D. Kini, B. Srivathsan and I. Walukiewicz. Using
non-convex approximations for efficient analysis of timed automata.
Proc. 31st Int. Conf. on Foundations of Software Technology and
Theoretical Computer Science (FSTTCS), 2011.
- [8] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient
Emptiness Check for Timed Büchi Automata. Formal Methods in System
Design (Special Issue Selected Papers CAV10 Conference), 40(2), 2012.
- [9] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better
abstractions for timed automata. Proc. 27th Symp. on Logic in Computer
Science (LICS), 2012.