| Titre : | Formal Modeling and Verification of Reconfigurable Systems |
| Auteurs : | Manel Houimli, Auteur ; Laïd Kahloul, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2025 |
| Format : | 1 vol. (94 p.) / ill., couv. ill. en coul / 30 cm |
| Langues: | Français |
| Langues originales: | Anglais |
| Résumé : |
The increasing complexity and dynamic nature of modern systems require advanced approaches to ensure their adaptability and efficiency. Reconfigurable systems, characterized bytheir ability to rapidly adjust to changing requirements, present significant challengesinmodeling,verification, and optimization. Numerous research efforts have focused on employingformal methods to tackle these challenges, aiming to enhance the reliability and performanceof these systems in diverse applications.Traditional formal methods, such as automata and classical Petri nets (PNs), have beeneffective for modeling and verification but struggle with the complexity of reconfigurable systems.Frequent structural changes require verification techniques that account for dynamic transitions.To address this, research has extended formalmethodstoincorporatereconfigurability,leading to new modeling and verification techniques (such as model checking extensions, probabilisticautomata, reconfigurability-based Petri nets extensions and Probabilistic Computation Tree Logic) tailored to these systems. Meanwhile, optimization techniques have been widely explored independently of formal verification to determine optimal configurations at differentreconfiguration stages. Methods like genetic algorithms and heuristic search optimize resourceallocation and performance but lack formal guarantees of correctness and safety. This gap highlightsthe need for approaches that combine optimization and formal verification to ensure bothefficiency and reliability in reconfigurable systems.In this thesis, we present two innovative approaches for modeling, verifying, and optimizingreconfigurable systems. The first contribution introduces a robust framework for modelingcommunication protocols at the Medium Access Control (MAC) layer of mobile wireless sensornetworks (MWSNs) and the MQTT protocol used in IoT applications. By utilizing probabilisticautomata for modeling and PCTL for property specification, we employ UPPAAL SMC forrigorous model checking. This approach not only enhances the reliability of these protocols butalso provides a systematic method for verifying critical properties, ultimately fostering trust inIoT applications.The second and major contribution proposes a novel formalism called Genetic Reconfigurable Object Nets (Gen-RONs), which enables the modeling and verification of the dynamicstructures of reconfigurable systems while optimizing them. By integrating formal modeling,verification, and optimization into a cohesive framework, we define mutation and crossoveroperationsof genetic algorithms through the formal firing of rule transitions in ReconfigurableObject Nets. This innovative approach significantly advances the capabilities of reconfigurablesystems, offering a comprehensive solution that addresses the complexities of dynamic reconfigurabilityalongside effective optimization strategies. |
| Sommaire : |
General Introduction 1 1 Comprehensive Overview of Reconfigurable Systems 6 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2 Reconfigurable Systems (RSs) . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.1 Characteristics of Reconfigurable Systems . . . . . . . . . . . . . . . . 8 1.2.2 Reconfigurability and its Underlying Principles . . . . . . . . . . . . . 8 1.2.3 Reconfigurability vs. Flexibility . . . . . . . . . . . . . . . . . . . . . 9 1.3 Classification of Reconfigurable Systems . . . . . . . . . . . . . . . . . . . . 10 1.3.1 Timing of Reconfiguration . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.2 Control Mechanism . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.3.3 Levels of Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 1.4 Reconfigurable Systems across Various Domains . . . . . . . . . . . . . . . . 11 1.5 Techniques and Methodologies for Reconfiguration . . . . . . . . . . . . . . . 12 1.6 Future Challenges in Reconfigurable Systems . . . . . . . . . . . . . . . . . . 13 1.7 Reconfigurability in Networking . . . . . . . . . . . . . . . . . . . . . . . . . 13 1.7.1 Mobile Wireless Sensor Networks (MWSNs) . . . . . . . . . . . . . . 14 1.7.2 Internet of Things and Reconfigurability . . . . . . . . . . . . . . . . . 17 1.8 Reconfigurable Manufacturing Systems (RMSs) . . . . . . . . . . . . . . . . . 19 1.8.1 Definition of Reconfigurable Manufacturing Systems (RMSs) . . . . . 19 1.8.2 RMS Key Characteristics . . . . . . . . . . . . . . . . . . . . . . . . . 20 1.8.3 Types of Reconfigurable Machines in RMS . . . . . . . . . . . . . . . 21 1.8.4 Performance Objectives in RMS Optimization . . . . . . . . . . . . . 22 1.9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2 Formal Methods and Genetic Algorithms 24 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2 Formal Methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.2.1 Formal Methods Overview . . . . . . . . . . . . . . . . . . . . . . . . 26 2.2.2 Formal Verification Using Model Checking . . . . . . . . . . . . . . . 27 2.2.3 Properties Specification Formalisms . . . . . . . . . . . . . . . . . . . 29 2.2.4 Formal Modeling Methods . . . . . . . . . . . . . . . . . . . . . . . . 33 2.3 Introduction to Genetic Algorithms . . . . . . . . . . . . . . . . . . . . . . . . 46 2.3.1 Fundamentals of Genetic Algorithms . . . . . . . . . . . . . . . . . . 46 2.3.2 Challenges in Applying GAs to RSs . . . . . . . . . . . . . . . . . . . 49 2.3.3 GAs Variants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 2.3.4 Multi-Objective Genetic Algorithms (MOGAs) . . . . . . . . . . . . . 51 2.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3 Model Checking for Formal Modeling and Verification of Reconfigurable Systems: Protocols Performance Evaluation 55 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.1.1 Context of the Work . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.2 Formal Verification of Collision Free Mobility Adaptive Protocol for Wireless Sensor Networks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 3.2.1 Formal Modeling Using TA and PTA . . . . . . . . . . . . . . . . . . 59 3.2.2 Qualitative Verification . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.2.3 Quantitative Verification . . . . . . . . . . . . . . . . . . . . . . . . . 65 3.2.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 3.3 Formal specification, verification and evaluation of the MQTT protocol in the Internet of Things . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 3.3.1 Structure of MQTT 3.1.1 packets . . . . . . . . . . . . . . . . . . . . 68 3.3.2 Informal Description of the MQTT 3.1.1 . . . . . . . . . . . . . . . . 69 3.3.3 Formal Modeling and Verification of MQTT 3.1.1 . . . . . . . . . . . 70 3.3.4 Formal Verification of MQTT 3.1.1 . . . . . . . . . . . . . . . . . . . 70 3.3.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74 3.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 4 On Formal Modeling, Analysis and Optimization of Reconfigurable Manufacturing Systems (RMSs) 76 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.2 Context of the Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.3 Basic concepts for modeling and optimization . . . . . . . . . . . . . . . . . . 81 4.3.1 Concepts for RMSs’ modeling . . . . . . . . . . . . . . . . . . . . . . 81 4.3.2 Concepts for RMSs’ optimization . . . . . . . . . . . . . . . . . . . . 83 4.4 Proposed approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 4.4.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 4.4.2 Problem Description . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 4.4.3 Problem Formulation . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 4.4.4 Genetic Reconfigurable Object Nets (Gen-RONs) . . . . . . . . . . . . 90 4.4.5 Properties Preservation through Crossover and Mutation Operators . . . 94 4.5 Gen-RONs based Genetic Algorithm . . . . . . . . . . . . . . . . . . . . . . . 95 4.5.1 Gen-RONs based NSGA-II principles . . . . . . . . . . . . . . . . . . 95 4.5.2 Entire Optimization Time Complexity . . . . . . . . . . . . . . . . . . 96 4.6 Experimentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 4.6.1 RMS Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 4.6.2 System Modeling Using Gen-RONs . . . . . . . . . . . . . . . . . . . 99 4.6.3 Example of a Configuration L-P/T Net . . . . . . . . . . . . . . . . . . 102 4.6.4 Performance Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . 103 4.6.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 4.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113 General Conclusion 114 Bibliography 117 |
| Type de document : | Thése doctorat |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/207 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
