On the Improvement of R-TNCESs Verification using Distributed Cloud-based Architecture

摘要

Reconfigurable discrete event control systems (RDECSs) are complex and critical systems, motivating the use of formal verification. This verification consists of two major steps: state space generation and state space analysis. The application of the mentioned steps is usually expensive in terms of computation time and memory. This paper deals with state space generation (accessibility graph generation) during verification of RDECSs modeled with specified reconfigurable timed net condition/event systems (R-TNCESs). We aim to improve model checking used for formal verification of RDECSs by proposing a new aproach of state space generation that considers similarities. 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.