AVeRTS - Algorithmic Verification of Real-Time Systems

AVeRTS in an Indo-French project on the algorithmic verification of real-time systems. The project is funded by CNRS on the french side, and by DST on the Indian side, under the CEFIPRA - Indo-French Program in ICST 2014-2016.

CNRS logo  DST logo CEFIPRA logoUB logo   LaBRI logo   INRIA logo  CMI logo  IITB logo

Members

Bordeaux
Rennes
Chennai
Mumbai
Frédéric Herbreteau Nathalie Bertrand B. Srivathsan S. Krishna
Igor Walukiewicz Blaise Genest
S. Akshay
Thanh Tung Tran Paulin Fournier
Ashutosh Trivedi



Devendra Bhave

Project leaders: Frédéric Herbreteau (LaBRI, France), S. Krishna (IIT Bombay, India)

Activity

Description of the project

Digital systems control most of the devices that surround us. Timing constraints are often crucial for cyber-physical systems that are designed to interact with the physical world. Correctness of cyber-physical systems that work under time-constraints is an ongoing challenge since traditional methods based on testing are no longer applicable in a safety-critical setting. This project aims at enlarging the applicability of formal verification for certifying correctness of timed systems. Formal verification requires that a system be modeled as a mathematical object. The model of timed automata has been introduced more than 25 years ago and has been an object of intensive study. It has also been successfully used in verification of cyber-physical systems.

The main scientific goal of the project is to enable control designers to exploit advances in formal verification of time critical cyber-physical systems. There have been several recent improvements to the existing state-of-the-art algorithms for verification of timed systems. We believe that these open up real opportunities to scale formal verification to larger and more complex systems. We plan to further improve the algorithms and integrate them in a tool that we are developing. In particular, we will take into account stochastic and distributed nature of modern cyber-physical systems. We also aim to apply these techniques to industrial-level applications.

Related publications by project members

Verification, games and synthesis for timed systems

Communicating/Distributed timed systems

Verification, games and synthesis for stochastic (timed) systems

Timed automata, languages and logics