Checking Missing-Data Errors in Cyber-Physical Systems Based on the Merged Process of Petri Nets
Checking Missing-Data Errors in Cyber-Physical Systems Based on the Merged Process of Petri Nets
复制标题
DOI：
10.1109/tii.2022.3181669
复制
发表时间：
2023-03
影响因子：
12.3
通讯作者：
Dongming Xiang;Shuai Lin;Xuehui Wang;Guanjun Liu
中科院分区：
文献类型：
--
作者：
Dongming Xiang;Shuai Lin;Xuehui Wang;Guanjun Liu
网络物理系统（CPS）中很容易发生丢失数据错误。尽管提出了许多基于业务流程建模符号（BPMN）的方法来对 CPS 进行建模并检测错误，但由于缺乏正式规范，很难自动验证其正确性，尤其是在数据流中。相比之下，Petri 网作为一种形式化方法，被广泛用于检测数据流错误。然而，这些方法很容易遇到状态空间爆炸问题。这主要是因为它们的可达图或状态转换图是基于交错语义的。合并过程作为Petri网的一种展开技术，可以刻画并发关系，缓解这一问题。因此，我们利用Petri网与数据的合并过程（PD-net）来检查CPS的丢失数据错误。我们首先将 CPS 的 BPMN 转换为 PD-net 并生成其合并过程。同时，我们分析其结构行为和数据相邻事件。此外，我们提出了一种检查丢失数据错误的算法。此外，还进行了案例研究和一些实验来证明我们方法的实用性和有效性。
Missing-data errors easily occur in cyber-physical systems (CPSs). Although many business process modeling notation (BPMN)-based methods are proposed to model CPSs and detect errors, it is hard to automatically verify their correctness, especially in the data flows, due to their lack of formal specifications. By comparison, Petri nets, as a formal method, are widely used to detect data-flow errors. However, these methods easily suffer from the state-space explosion problem. This is mainly because their reachability graphs or state transition graphs are based on the interleaving semantics. As an unfolding technique of Petri net, a merged process can characterize concurrency relations and alleviate this problem. Thus, we utilize the merged process of Petri net with data (PD-net) to check the missing-data errors of the CPS. We first transform a BPMN of the CPS into a PD-net and generate its merged process. Meanwhile, we analyze its structural behaviors and data-adjacent events. Furthermore, we propose an algorithm for checking missing-data errors. In addition, a case study and some experiments are done to show the practicality and effectiveness of our method.