Minotor: Monitoring Timing and Behavioral Properties for Dependable Distributed Systems

International audienceAssessing the correct behavior of a given system at run-time can be achieved by monitoring its execution, and is complementary to off-line analysis such as static verification. In this work, we focus on run-time monitoring of system properties that include both causality and timing constraints, in distributed and time-constrained systems. Based on a description of a property that includes events and temporal constraints, expressed as a timed-arc Petri net, we show how to automati- cally transform it into a an executable and distributed monitoring engine. To that aim, we introduce a modification of the semantics of Petri nets to be able to execute it online on partial executions and distributed observation environments. We show how to use this formal frame- work to provide Minotor, a model-driven distributed monitoring system, describe its implementation and show its applicability on a transportation use-case