Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL

This paper addresses the formal verification of reconfigurable discrete event systems (RDESs) using Isabelle/HOL proof assistant. A reconfigurable system transitions from one mode to another during its operation to adapt its behavior to the relevant environment. By including such a feature, RDESs become complex and are often costly in terms of computation time and memory. The verification of RDESs consists of two main steps: state space generation and state space analysis. In order to improve these two steps, we propose in this paper, a new approach for verifying system properties that is performed on a developed distributed architecture. The proposed approach allows to avoid redundant computation and reduce execution time by considering the relationships between properties and creating a parallel algorithm that ensures a suitable execution order for each property that is not costly and efficient. The proposed approach is evaluated by exploiting a case study that illustrates the impact of using this approach. The results demonstrate the significance of this paper.