TiCKTaC

Efficient Techniques and Tools for the Verification and Synthesis of Real-Time Systems

The Automata and Applications team of LRE participated in the ANR-funded TiCKTaC project (2019–2023), which aimed to improve formal verification and synthesis of real-time systems using the timed automata formalism. The project focused on developing novel algorithms, alternative data structures, and richer specification techniques to enhance scalability and expressiveness in verifying systems with quantitative features such as execution time and energy consumption. The project produced an open-source model checker, TChecker, implementing these advances and enabling systematic comparison of tools and algorithms. TiCKTaC applied its methods to practical case studies, including robotics planning and performance verification in train networks, validating the new algorithms and demonstrating their effectiveness on large-scale, real-world systems. TiCKTaC was strongly committed to open science: all tools and software developed during the project were released under open-source licenses, facilitating reuse and further development by the research community.