The TickTac project aims to design efficient algorithms and softwares for the analysis of timed automata.
We are developing several open-source softwares:
- TChecker is a framework for the implementation of verification algorithms for real-time systems. In particular, it proposes a command-line tool that implements a covering reachability algorithm (see the wiki page using tchecker).
- tcltl is an LTL model-checker based on the TChecker library and Spot. TChecker is used to produce the state-space of the system while Spot checks the satisfiability of the LTL formula.
- uppaal-to-tchecker can be used to translate Uppaal models into TChecker file format.
The project is also proposing a benchmark of test-cases.