{'fraction_non_alphanumeric': 0.020242914979757085, 'fraction_numerical': 0.0, 'mean_word_length': 5.591111111111111, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the Improvement of R-TNCESs Verification using Distributed Cloud-based Architecture

: Reconﬁgurable discrete event control systems (RDECSs) are complex and critical systems, motivating the use of formal veriﬁcation. This veriﬁcation 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 veriﬁcation of RDECSs modeled with speciﬁed reconﬁgurable timed net condition/event systems (R-TNCESs). We aim to improve model checking used for formal veriﬁcation 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 veriﬁcation. A distributed cloud-based architecture is proposed to perform the parallel computation for control veriﬁcation time and memory occupation. The paper’s contribution is applied to a benchmark production system. The evaluation of the proposed approach is performed by measur-ing the temporal complexity of several large scale system veriﬁcation. The results show the relevance of this approach.