R-TNCES State Space Generation Using Ontology-Based Method on a Distributed Cloud-Based Architecture

This paper deals with formal verification (accessibility graph generation & state space analysis) of RDECSs modeled with specified reconfigurable timed net condition/event systems (R-TNCESs) where the properties to be verified to ensure the well behave of systems are expressed by computation tree logic CTL. Reconfigurable discrete event control systems (RDECSs) are complex and critical systems, which, make their formal verification expensive in terms of complexity and memory occupation. We aim to improve model checking used for formal verification of RDECSs by proposing a new approach of state space generation that considers similarities and a parallel verification of CTL properties. In this approach, we introduce the modularity concept for verifying systems by constructing incrementally their accessibility graphs. Furthermore, we set up an ontology-based history to deal with similarities between two or several systems by reusing state spaces of similar components that are computed during previous verification. A distributed cloud-based architecture is proposed to perform the parallel computation for control verification time and memory occupation. The paper’s contribution is applied to a benchmark production system. The evaluation of the proposed approach is performed by measuring the temporal complexity of several large scale system verification. The results show the relevance of this approach.