Nicolas Markey

Résumé

In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.

@inproceedings{rv2024-HJMR,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas and Roussanaly, Victor},
  title =               {Distributed Monitoring of Timed Properties},
  editor =              {{\'A}brah{\'a}m, Erikz and Abbas, Houssam},
  booktitle =           {{P}roceedings of the 24th {I}nternational {W}orkshop
                         on {R}untime {V}erification ({RV}'24)},
  acronym =             {{RV}'24},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {15191},
  pages =               {243-261},
  year =                {2024},
  month =               oct,
  doi =                 {10.1007/978-3-031-74234-7_16},
  abstract =            {In formal verification, runtime monitoring consists
                         of observing the execution of a system in order to
                         decide as quickly as possible whether or not it
                         satisfies a given property. We consider monitoring
                         in a distributed setting, for properties given as
                         reachability timed automata. In~such a setting,
                         the~system is made of several components, each
                         equipped with its own local clock and monitor.
                         The~monitors observe events occurring on their
                         associated component, and receive timestamped events
                         from other monitors through FIFO channels. Since
                         clocks are local, they cannot be perfectly
                         synchronized, resulting in imprecise timestamps.
                         Consequently, they must be seen as intervals,
                         leading monitors to consider possible reorderings of
                         events. In this context, each monitor aims to
                         provide, as early as possible, a verdict on the
                         property it is monitoring, based on its potentially
                         incomplete and imprecise knowledge of the current
                         execution. In~this~paper, we~propose an on-line
                         monitoring algorithm for timed properties, robust to
                         time imprecision and partial information from
                         distant components. We~first identify the date at
                         which a monitor can safely compute a verdict based
                         on received events. We~then propose a monitoring
                         algorithm that updates this date when new
                         information arrives, maintains the current set of
                         states in which the property can reside, and updates
                         its verdict accordingly.},
}