Modelisation et verification Formelles des systemes critiques

The acceleration of technological progress and the increasing integration of systems have made critical systems ubiquitous in essential areas such as healthcare, transportation, and infrastructure. The reliability of these systems is crucial, as failures can have significant reper-cussions. In light of these challenges, it is essential to adopt rigorous methods to ensure their safety and reliability. Among the various approaches, formal methods stand out for their ability to provide an unmatched level of confidence regarding the behavior of critical systems. In this thesis, we explore the use of formal methods for the modeling and verification of critical systems, aiming to propose a comprehensive methodology that combines the power of graphical modeling tools with the rigor of these methods. Our approach is structured around three main contributions. First, we developed a design method for critical systems that promotes rigorous version management while allowing for the gradual integration of new features. Next, we integrated modeling tools such as UML (Unified Modeling Language) and OCL (Object Constraint Language), as well as Petri nets, with formal methods. This approach optimizes the readability of models while ensuring the necessary rigor to meet safety requirements. Finally, we formalized and implemented the Clark-Wilson security policy within a robust framework, thereby protecting critical systems against internal and external threats while ensuring verifiable compliance with security standards. These contributions are illustrated by various case studies, demonstrating the effectiveness of our approach.