Time Supervision of Concurrent Systems using Symbolic Unfoldings of Time Petri Nets
Résumé
Monitoring real-time concurrent systems is a challenging task. In this paper we formulate (model-based) supervision by means of hidden state history reconstruction, from event (e.g. alarm) observations. We follow a so-called true concurrency approach using time Petri nets: the model defines explicitly the causality and concurrency relations between the observable events, produced by the system under supervision on different points of observation, and constrained by time aspects. The problem is to compute on-the-fly the different partial order histories, which are the possible explanations of the observable events. We do not impose that time is observable: the aim of supervision is to infer the partial ordering of the events and their possible firing dates. This is achieved by considering a model of the system under supervision, given as a time Petri net, and the on-the-fly construction of an unfolding, guided by the observations. Using a symbolic representation, this paper presents a new definition of the unfolding of time Petri nets with dense time. // La supervision des systèmes distribués temps réel est une problème d'actualité. Dans ce papier nous abordons la supervision sous forme de reconstruction d'histoires à partir d'observation d'événements (par exemple d'alarmes). Nous proposons une approche de vraie concurrence utilisant les réseaux de Petri temporels : le modèle définit explicitement les relations de causalité et de concurrence entre les événements observables émis par le système qui est observé par plusieurs capteurs et qui est contraint par des aspects temporels. Le problème consiste à calculer au vol les différentes histoires (sous forme d'ordre partiel) qui peuvent expliquer les événements observés. Nous n'imposons pas que le temps soit observable : le but de la supervision est d'inférer l'ordre partiel des événements et les dates de tir possibles. Pour cela nous considérons un modèle du système à superviser, donné sous la forme d'un réseau de Petri temporel, et nous construisons au vol un dépliage guidé par les observations. Cet article présente une nouvelle définition du dépliage d'un réseau de Petri temporel, dans lequel le temps est représenté de manière symbolique.
Loading...