From LaBRI - Laboratoire Bordelais de Recherche en Informatique

Theses: 2013FalconeMosbahRollet

Runtime validation of timed properties


In a general way, the objective of this PhD position is to extend runtime verification and enforcement in the context of timed systems and complete the picture of theoretical results.

Some questions still remain open. Which timed properties can be monitored / enforced? How the set of enforeable/monitorable properties evolves according to the architecture and under different enforcement primitives for the monitor? How can we synthesize an enforcement monitors from descriptive specifications. Intuitively, in runtime enforcement, one of the difficulties is that the operations of the enforcer influence the timings constraints of the initial behavior.

The main objective of this work is to provide a complete framework of monitoring / enforcement of timed systems, with several kinds of timed properties (safety, co-safety, and more expressive properties...) described in timed temporal logics and using several transparency rules. The implementability of this approach should also be investigated.

Theoretical results shoud be supported by a tool in order to demonstrate the effectiveness of the proposed approaches.

Récupéré sur
Page mise à jour le 19/10/2012 à 10:02