Modelling and analysis of real-time, hybrid and probabilistic systems. Software tools for and applications of the above. Typical applications include control systems, robotics, mobile networks, biological systems. The goal of my research is (a) to develop the foundations for analyzing hybrid systems and (b) to facilitate design and verification of actual systems by creating software tools for synthesis, simulation, and verification.
The
Timed I/O Automaton Language (TIOA)
provides the semantic basis for the
Tempo Toolset.
This toolset is being implemented by researchers at MIT, UConn, and
VeroModo Inc.
The toolset currently consists of a
simulator for TIOA specifications,
an interface to the
UPPAAL model checker,
and an interface to the
PVS theorem prover.
I have contributed to the development of the TIOA Language and the PVS-interface.
For example, the translation scheme of
this paper and the strategies
proposed in
this paper are embodied in the current version of the Tempo toolset.
In this page
I intend to collect benchmarks for hybrid systems analysis tools.