Monitoring cyber-physical systems using formal methods

Monitoring cyber-physical systems consists in deciding whether a property is satisfied along one log, i.e., a sequence of samples ordered with time. Monitoring attracts both scientific and practical attention. However, monitoring algorithms suffer from the methodological difficulty of only observing sampled discrete-time signals gathered in a log, while real behaviors are continuous-time signals, which implies some uncertainty.

In addition, the monitoring properties can themselves feature some uncertainty: e.g., a period in a property to be monitored can be uncertain or even unknown. In this presentation, I will first present a global state of the art of the challenges related to monitoring using formal methods. I will then present two ways to address uncertainty while monitoring cyber-physical systems.