Formal Modeling and Verification of Reconfigurable Systems

Houimli, Manel (2025) Formal Modeling and Verification of Reconfigurable Systems. Doctoral thesis, Université Mohamed Khider (Biskra - Algérie).

Text HouimliThesis.pdf Download (2MB)

Abstract

The increasing complexity and dynamic nature of modern systems require advanced approaches to ensure their adaptability and efficiency. Reconfigurable systems, characterized by their ability to rapidly adjust to changing requirements, present significant challenges in modeling, verification, and optimization. Numerous research efforts have focused on employing formal methods to tackle these challenges, aiming to enhance the reliability and performance of these systems in diverse applications. Traditional formal methods, such as automata and classical Petri nets (PNs), have been effective 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 formal methods to incorporate reconfigurability, leading to new modeling and verification techniques (such as model checking extensions, probabilistic automata, 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 different reconfiguration stages. Methods like genetic algorithms and heuristic search optimize resource allocation and performance but lack formal guarantees of correctness and safety. This gap highlights the need for approaches that combine optimization and formal verification to ensure both efficiency and reliability in reconfigurable systems. In this thesis, we present two innovative approaches for modeling, verifying, and optimizing reconfigurable systems. The first contribution introduces a robust framework for modeling communication protocols at the Medium Access Control (MAC) layer of mobile wireless sensor networks (MWSNs) and the MQTT protocol used in IoT applications. By utilizing probabilistic automata for modeling and PCTL for property specification, we employ UPPAAL SMC for rigorous model checking. This approach not only enhances the reliability of these protocols but also provides a systematic method for verifying critical properties, ultimately fostering trust in IoT 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 dynamic structures of reconfigurable systems while optimizing them. By integrating formal modeling, verification, and optimization into a cohesive framework, we define mutation and crossover operations of genetic algorithms through the formal firing of rule transitions in Reconfigurable Object Nets. This innovative approach significantly advances the capabilities of reconfigurable systems, offering a comprehensive solution that addresses the complexities of dynamic reconfigurability alongside effective optimization strategies.

Actions (login required)

View Item