6 mars 2023
Etienne André (LIPN, Université Sorbonne Paris Nord)Monitoring cyber-physical systems 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, we present two ways to address uncertainty while monitoring cyber-physical systems.
First, we address timed pattern matching in the presence of an uncertain specification. We want to know for which start and end dates in a log, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum period (together with the corresponding start and end dates) for which the property holds.
We rely on two solutions, one based on model-checking, and the other one being ad-hoc.
Second, to mitigate the problem of sampling uncertainties, we introduce a model-bounded monitoring scheme, where we use a (limited) prior knowledge about the target system in order to prune interpolation candidates. We express such prior knowledge by linear hybrid automata (LHAs)—the LHAs are called bounding models. We rely on reachability techniques for linear hybrid automata using polyhedra to efficiently decide whether the property holds on a given log.
We implemented both approaches, and experiments on realistic benchmarks show that both directions are efficient and practically relevant.
This presentation is mainly based on publications at ICECCS 2018 and ACM ToCPS (2022), and are joint work with Masaki Waga (Kyoto University) and Ichiro Hasuo (NII, Tokyo, Japan).