Efficient Verification of Timed Automata

Résumé

Timed automata are finite automata extended with clocks that can be reset and tested on the transitions. Clocks hence measure 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 executions of the automaton. The efficiency of the verification algorithms heavily rely on the coarseness of the abstraction. These last years, we have proposed several optimizations of the abstractions and the underlying algorithms. The goals of this thesis are:

  • to develop new abstractions that dynamically use the informations collected by verification algorithms,
  • to study which are the properties preserved by these abstractions,
  • the combination to verification techniques for distributed systems.

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.
Page mise à jour le 19/10/2012 à 17:08