A Formal Coloured Petri Net Model for Hazard Detection in Large Event Flows

This paper deals with a formal approach for the detection of situations in the context of complex event processing, which is a technique particularly employed in the aerospace field. Indeed, aerospace systems generally involve numerous interacting agents, to each of which are associated various possible events, thus yielding a huge flow of events. A common issue when dealing with the safety of such systems consists in being able to detect in this flow certain event correlations, from which one may then deduce that the system is in a particular (often critical or hazardous) state. This work is based on a situation description language called chronicles, and provides for it a formal recognition model based on coloured Petri nets. A two-layer compositional model is provided: a concurrent, nondeterministic recognition model for each chronicle construct, together with additional control structures allowing to overview the recognition treatments performed on the event flow.