Overview
This Web page is dedicated to the project CATS (Compositional Analysis of Timed Systems) taking place in 2013−2014.
It involves scientists from Hồ Chí Minh City University of Technology, LIPN, NTU, NUS and SUTD.
This project is mainly supported by the STIC Asie program by Ministère français des affaires étrangères and CNRS.
Goal
The main challenge for verification is state explosion, viz., the explosion of the number of possible states to consider in order to be able to formally verifying a system. A possible way to reduce state explosion is to consider modular or compositional verification: each subpart of the global system is verified separately and, after some additional operations, one is able to prove the correctness of the global system. Real-time systems are more complex than untimed systems and suffer from clock explosion. Most compositional techniques developed for untimed systems have had very limited success with timed systems.
Timed automata and time Petri nets are two established modeling formalisms for timed systems. Based on previous work, we shall attempt to combine our expertise to identify a class of timed automata and of time Petri nets, expressive enough to be practical, and that make compositional verification more successful.
Collaboration is sought on both the theory and tool implementation, and these techniques and algorithms should be implemented. Different tools developed at LIPN and at NUS can be used as a basis for our implementations.
Evaluation of our techniques will be performed in the framework of automated assistance of frail aging people, in collaboration with Singapore hospitals.
