Verifying Timed Automata

Supervisor

James Worrell

Suitable for

Abstract

The goal of this project is to build a tool for simulation and verification of real-time systems modelled as timed automata.   The tool would use symbolic techniques, including SAT solving, to analyse continuous-time systems.

This project would suit a student taking courses in Computer-Aided Formal Verification or Automata, Logics and Games.

 Reading:

 Rajeev Alur: Timed Automata. CAV 1999, LNCS 1633, Springer 1999.

 E. Clarke, O. Grumberg and D. Peled.  Model Checking (Chapter 17).  MIT Press 2002.