Modélisation et vérification formelles des systèmes critiques

الموضوعات

علوم تطبيقية وتكنولوجية

الملخص

L’accélération du progrès technologique a rendu les systèmes critiques, de plus en plus intégrés, omniprésents dans des domaines essentiels tels que la santé, les transports et les infrastructures. La fiabilité de ces systèmes est cruciale, car les défaillances peuvent avoir des répercussions considérables. Face à ces enjeux, il est essentiel d’adopter des méthodes rigoureuses pour garantir leur sûreté et leur fiabilité. Parmi les différentes approches, les méthodes formelles se distinguent par leur capacité à offrir un niveau de confiance inégalé concernant le comportement des systèmes critiques. Dans cette thèse, nous explorons l’utilisation des méthodes formelles pour la modélisation et la vérification des systèmes critiques, visant à proposer une méthodologie complète qui allie la puissance des outils de modélisation graphiques à la rigueur de ces méthodes. Notre démarche se structure autour de trois contributions principales. Premièrement, nous avons développé une méthode de conception de systèmes critiques, favorisant une gestion rigoureuse des versions tout en permettant une intégration progressive des nouvelles fonctionnalités. Ensuite, nous avons intégré des outils de modélisation tels que UML (Unified Modeling Language) et OCL (Object Constraint Language), ainsi que des réseaux de Petri, avec des méthodes formelles. Cette approche optimise la lisibilité des modèles tout en garantissant la rigueur nécessaire pour répondre aux exigences de sûreté. Enfin, nous avons formalisé et mis en œuvre la politique de sécurité Clark-Wilson dans un cadre robuste, protégeant ainsi les systèmes critiques contre les menaces internes et externes tout en assurant une conformité vérifiable aux normes de sécurité. Ces contributions sont illustrées par des études de cas variées, démontrant l’efficacité de notre approche. (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).

روابط وملفات

التعريف والنوع

رقم الوثيقة

02743e86-29ce-4ab7-9af3-b936ac3a3f95

رقم العقد

0

نوع الوسائط

Crawler

نوع المحتوى

الرسائل العلمية

صيغة المصدر

رسائل دكتوراة

نوع الملف

pdf image

أسماء الملفات

1034249_1.pdf

بيانات النشر

ألقاب المؤلفين

[{"name_ar":"Ammar Boucherit","title_ar":"اشراف","title_en":"Supervision"},{"name_ar":"Fatima Haloua","title_ar":"اعداد","title_en":"Preparation"},{"name_ar":"Messaoud Abbas","title_ar":"اشراف","title_en":"Supervision"}]

اللغة

French

المصدر والدورية

اسم المصدر

Modélisation et vérification formelles des systèmes critiques

المحتوى والصفحات

عدد الصفحات

0

ترجمة الملخص

إن عصر التقدم التكنولوجي المتسارع الذي نعيشه جعل من الأنظمة الحساسة أكثر تكاملا وانتشارا في مجالات أساسية شتى مثل الصحة والنقل والبنية التحتية. حيث تعتبر موثوقية هذه الأنظمة أمرًا بالغ الأهمية، لأن الإخفاقات فيها قد تكون لها آثار جسيمة سواء كانت مادية او بشرية وبالنظر إلى هذه التحديات، من الضروري اعتماد أساليب صارمة لضمان سلامة وموثوقية هذه الأنظمة. من بين الأساليب المختلفة المعتمدة، تتميز الأساليب الرسمية بقدرتها على توفير مستوى غير مسبوق من الثقة في سلوك الأنظمة الحساسة.في هذه الأطروحة، استكشف استخدام الأساليب الرسية في النمذجة والتحقق من الأنظمة الحساسة، بهدف تقديم منهجية متكاملة تجمع بين قوة أدوات النمذجة الرسمية ودقة هذه الأساليب.تتمحور منهجيتنا حول ثلاث مساهمات رئيسية أولاً، قمنا بتطوير منهجية لتصميم الأنظمة الحساسة، تتيح إدارة صارمة للإصدارات مع السماح بالتكامل التدريجي للوظائف الجديدة. ثانيا، قمنا بدمج أدوات النمذجة مثل UML و OCL . بالإضافة إلى شبكات Petri ، مع الأساليب الرسية. يعزز هذا النهج وضوح النماذج مع ضمان الدقة اللازمة لتلبية متطلبات السلامة. وأخيرا، قمنا بتطبيق وتوثيق سياسة الأمان الخاصة بـ Clark Wilson ضمن إطار عمل متين، مما يضمن حماية الأنظمة الحساسة من التهديدات الداخلية والخارجية، مع الالتزام بمعايير الأمان القابلة للتحقق.وقد تم توضيح هذه المساهمات من خلال تطبيقها على ثلاث دراسات حالة متنوعة، مما أثبت نجاحها في تحسين موثوقية الأنظمة الحساسة. هذه النتائج تعزز أهمية استخدام الأساليب الرسمية لضمان أمان الأنظمة وتعزيز قدرتها على مواجهة التحديات المستقبلية.

كلمات الباحثين

Systèmes critiques, méthodes formelles, modélisation et vérification, UML, réseaux de Petri, politique de sécurité Clark-Wilson.

إشراف وإعداد

الإشراف

Ammar Boucherit, Messaoud Abbas

الإعداد

Fatima Haloua

الاقتباسات الببليوغرافية