Contributions to formal analysis and diagnosis from colored Petri nets with backward accessibility.

Summary The rapid development of embedded systems and the increasing requirements to which they are subjected create a need for innovative techniques in terms of design, verification and validation. Formal methods provide interesting approaches to the design of these systems, especially for dependability studies. The chosen formalism is based on Colored Petri nets (CPN). The advantage of these models, in addition to being very expressive and formal, is that they can express the dual character of the systems studied: static and dynamic. The challenge of this thesis is to use established models, describing the architecture and/or the behavior of systems, to extract SoF information in general and failure diagnosis in particular. The proposed approach is a structural analysis by backward accessibility of RdPC. It can be decomposed into two parts. The first is the proposal of a tool to perform this analysis: the reverse RoPc. It is obtained through the application of structural transformations on the original RdPC. The second part is the implementation of the analysis. This part requires complementary mechanisms, the most important of which is the enrichment of the marking. The proposed approach is studied from two complementary points of view: algorithmic and theoretical. The algorithmic point of view consists in proposing models of transformations for the inversion of the RoPc and the implementation of the analysis. The theoretical aspect aims at providing a formal basis for the approach by applying two methods (linear algebra and linear logic) to prove our approach.