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

Formal verification, in particular model checking, consists in proving the correctness of safety critical systems. The correctness of several classes of real-time systems depend not only on whether the system computes the right output, but also on quantitative measures such as execution time, and energy consumption. Most finite-state verification formalisms allow designers to define some notion of time, often by discretization of the time domain; however, such notions of time may lack precision in the modeling and when it is precise enough it tends to produce large finite-state systems that even cutting-edge techniques cannot handle adequately. It is thus crucial to develop specialized techniques for real-time systems with such quantitative features with a focus on improving the expressiveness and the scalability of formal verification with respect to existing techniques.

Timed automata are a standard formalism for modeling such systems with explicit time constraints, for which algorithms and tools have been developed.
These tools have had an impressive impact in the formal verification of real-time systems and have been used in industrial collaborations. However, some barriers that prevent timed automata verification to scale to even larger systems and real-size industrial applications remain. In fact, although current techniques can handle complex time constraints, the scalability with respect to the size of the discrete state space is a real issue; many succesful ideas from the model checking community, such as abstraction refinement, dynamic abstractions, partial-order reduction have not been fully exploited.
Efficient verification of liveness and quantitative optimization problems have not been given necessary attention either, making model checkers' capabilities less attractive. Moreover, state-of-the-art model checkers mostly rely on same formalisms and do not explore possibilities for tailoring alternative algorithms with complementary efficiency, or efficient solutions for particular classes of systems.

The goal of this project is to overcome some of these obstacles in the scalability of verification and synthesis algorithms for timed automata by studying novel algorithms, alternative data structures, richer specifications, systematic abstraction techniques, while working on case studies that range from planning in robotics, performance verification in train networks, and in other collaborations we have with our partners. These will guide and validate the developed algorithms. At the heart of our project is the development of an open source model checker that is up-to-date, contains our new algorithms, which handles several extensions of the formalism such as optimization and synthesis problems. The model checker will use the same input format as existing tools to allow one to systematically compare the performance of tools and algorithms. We build our work on the experience of the consortium members which are responsible for several recent advances and state-of-the-art algorithms for timed automata verification, and also have experience in tool development. Our goal is to make timed automata verification and synthesis more attractive by enriching the allowed modeling and specifications features, and by developing techniques that scale to large systems, making the timed automata technology the tool of choice for the formal verification of real-time systems.