Context
Timed automata and time Petri nets are fundamental formal models for real-time systems. Since the seminal work of Alur and Dill (1994), the theory has progressed and mature analysis tools like UPPAAL are now of industrial strength. These tools can verify quantitative properties of real-life real-time systems.
The game extension of timed automata has also received a lot of attention in the last 2 decades. The objective for games is to synthesise real-time controllers (or strategies) rather than verify a real-time system. Synthesis for timed automata (and time petri nets) has been a successful domain and UPPAAL has a game extension UPPAAL-TiGA to synthesise real- time controllers.
The current challenging problems are to synthesize controllers for systems that are partially observable and optimal controllers with respect to a given criterion. Extensions of timed automata with weights (e.g. to model energy consumption) have been extensively studied in the last five years. Synthesis of optimal controllers is also a very active topics.
Approach
Our work spans accross different theoretical and practical aspects among them:
- Formal models for timed systems: this amounts to comparing the expressive power of different formalisms for timed systems;
- Analysis of partially observable timed systems: this line of work has applications in fault diagnosis and controller synthesis under partial observation. We contribute both theoretical results and practical implementations in UPPAAL or UPPAAL-TiGA.
- Optimal controller synthesis: synthesis of controllers for energy or mean payoff timed games.
- Worst-case execution time analysis (WCET): This topic spans accross program anaylsis and timing analysis and is developed as a separate project WCET
Tools
The results of this research have been continuously transfered into timed systems analysis tools, UPPAAL, UPPAAL-TiGA and ROMEO. Case studies have been successfully treated with the approaches we proposed. Related verification/synthesis tools for timed systems:
- UPPAAL Model Checking of Timed Automata
- UPPAAL-TiGA Efficient Controller Synthesis for Timed Automata
- KRONOS Model-Checking for Timed Automata
- HyTech Reachability analysis for Hybrid Automata. Here is a tgz hytech-for-osX.tgz for compiling HyTech under Mac OS X (unofficial version). To use see the README-OSX in src directory.
- PHAver Polyhedral Hybrid Automaton Verifyer (and How to Install it for Mac OSX)
- Roméo A tool for Time Petri Nets analysis
- Tina TIme petri Net Analyzer
- TIMES Tool for Modeling and Implementation of Embedded Systems
Collaborations
Aalborg University, Denmark; LSV-ENS Cachan, France; Université Libre de Bruxelles, Belgium; IRCCyN, Nantes, France; INRIA, Rennes, France
