000 02202 a2200157 4500
003 DZ-ElOued
005 20260602171332.0
100 1 _aAbbas, Messaoud
700 1 _aHaloua, Fatima
245 0 0 _aModelisation et verification Formelles des systemes critiques
260 _b
_c2025
500 _aModelisation et verification Formelles des systemes critiques
520 _aThe 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.
650 4 _a/Modelisation//et//verification//Formelles//des//systemes//critiques/
942 _cTHESIS
999 _c18633
_d18633