Modélisation et Évaluation Analytique du Temps de Réponse des Systèmes de Contrôle-Commande Distribués en utilisant des Réseaux de Petri et l'Algèbre des Dioïdes

The problem addressed in this thesis concerns above all the analytical evaluation of a response time bound for a distributed control system, in a critical industrial context. The teleology of the work is therefore to prove this bound by a method that must be based on two aspects: a modelling based on a graphical formalism (that can be simulated), and a calculation derived from mathematical descriptions of the model. In the literature, classical methods of formal verification generate combinatorial explosion: thus in this work, we turn to algebraic methods.Within the latter, the tropical algebra provides interesting elements for the description of Timed Event Graphs (TEGs), since their representation is linear in this algebra. However, this class of Petri nets can only model synchronization and parallelism phenomena. Although these phenomena are common in a control system, they are only part of what is interesting to model. Consequently, after demonstrating the feasibility of an approach based on the algebraic description of GET models using the formal series dioid, we propose to construct a similar dioid for the description of Timed Colored Petri nets (TCPNs), a much broader class because high-level and interpretable. Following the Kleene-Schützenberger theorem, we construct formal coloured series (FCS), and, by proof of their rationality, we show that they realize the behaviour of a subclass of linear RPCTs in tropical algebra. In addition, we explain the links between an RPCT model and its implementation in SFC trajectories.These SFCs are built around a total order arbitrarily imposed on the set of colors in a model, and interpreted as the order of priorities. In this way, we can express colour shifts and make the behaviour of an RPCT model completely deterministic (even for the non-linear case).SFC trajectories can be used to establish laws/functions/algorithms that perform non-linear operations in tropical algebra, induced by phenomena other than synchronization or parallelism (such as conflict, competition, resource sharing, partial synchronization, multiplicities, etc.). In particular, these non-linear operations express the order shifts induced on trajectories. Without being exhaustive, we present various cases of non-linear mechanism management to show that the use of SFCs offers broader capabilities than those obtained by the classical series associated with GET. Finally, we give some examples of delay calculations in coloured models that can be integrated into the method. In particular, we model a switched network in RPCT and propose its trajectory setting. Using predictability assumptions, we then calculate the end-to-end travel time in the worst-case scenario.Furthermore, the proposed approach is modular. The behaviour of linear parts can be computed via the classical theory of dioids, developed through GET, and ensuring the simplification of any linear model into a transfer function, the latter being the smallest solution of the system of linear equations associated with the model. The behaviour of the non-linear parts can be calculated by the new operations we define (convolution, iterative algorithms, trajectory reductions, reordering, etc.). The concept of trajectory then ensures interoperability between the different parts: for any operation taking trajectories as inputs, and constructing them as outputs, it is possible to consider this operation in isolation within the calculation of a system's behaviour.