Behavioural Analysis for Distributed Simulations

This paper focuses on an application of formal methods: behavior detection, where a formal language is used to describe behaviors within a system, together with formal recognition rules used to detect these described behaviors within an event flow resulting from the operation of the system. This formal approach is very interesting for aerospace system studies: these generally involve numerous interacting agents and are thus very complex. Since actual systems are too expensive or too critical to be directly studied, they require simulations. Formal behavior detection is a convenient method allowing, in a non-intrusive way, to evidence within a very complex simulation the data necessary to understand finely the behavior of some agents. This data may be used to evidence integration problems in the simulation, or to exploit its results. We present an application where formal behavior detection has proven to be very beneficial, and the formal framework used, namely a description language called chronicles and an operational recognition model provided by a modular coloured Petri net semantics, which we prove to be adequate with the set definition of the recognition notion.