The timed and hybrid systems group at VERIMAG is interested in all aspects of system design, ranging from theoretical foundation, via design techniques, down to implementation. In terms of models, the group’s domain of research is characterized by two major extensions to the discrete models, such as automata, traditionally used to describe systems, namely timed and hybrid systems.
Timed Systems
Purely discrete models such as automata can only express system behaviors in a qualitative manner, i.e. ordering between events. They cannot express quantitative (metric) properties that speak about the time elapsed between two events. In other words, the behaviors are not embedded in the real-time axis. The theory of timed automata, automata augmented with clock variables that measure the time the automaton spends in certain states, has proved to be very effective in modeling a large range of phenomena in diverse domains such as real-time programs, scheduling in manufacturing systems and digital circuit timing analysis. Members of our group introduced the first verification tool for timed automata, Kronos, in 1990, and since then we continue to work on all aspects of the domain.
Among our results in timed systems one can find the definition of specification formalisms for timed behaviors such as real-time temporal logics and timed regular expressions, the development of symbolic model-checking algorithms for timed automata, the efficient implementation of these algorithms using special data-structures for storing zones (a special type of polyhedra for storing sets of clock valuations), the development of a compiled on-the-fly version of Kronos (OpenKronos), the modeling and verification of dozens of case-studies, the development of a modeling framework for composing and scheduling real-time software, development of shortest path algorithms for timed automata and applying them to scheduling problems.
In recent years some of the timed systems technology has been transferred toward industry. The timed component of the tool IF, developed and maintained by the DCS groups of VERIMAG is used for verifying SDL programs. Within the TAXYS project, some of the Kronos technology has been integrated into a compiler for the Esterel language in order to check schedulability at compile time. Other applications to multi-threaded Java programs are currently being investigated. We believe that timed automata provide an excellent level of abstraction for phenomena in diverse domains and that they can serve as a unifying model for many problems.
Hybrid Systems
Hybrid systems take us further away from discrete systems to the domain of continuous dynamical systems as used by control engineers to model the environments they want to control as well as certain parts of the controllers. It has been recognized by the control community that purely-continuous models are not sufficient for describing and analyzing such systems throughout all their operation region. There many "logical" features that interfere with the model due to "mode switching", saturation of sensors and actuators, faults, discrete phenomena such as collisions and more. While the theory of differential equations gives a respectable mathematical support for continuous control, such hybrid systems with switching phenomena are usually left to the mercy of hackers. In 1990, members of our group proposed the hybrid automaton model, which can be viewed as an extension of the timed automaton, that is, an automaton with continuous variables that evolve according to a distinct differential equation in each state of the automaton. Much of our work in the domain is concerned with the extension of verification methodology to such continuous and hybrid domains, a task far from being trivial due to the completely different nature of the state-space and trajectories of continuous systems. Due to the novelty of the approach and the exploratory and inter-disciplinary nature of the research, the tools developed by our group are no yet mature for real industrial applications.
