Checking Missing-Data Errors in Cyber-Physical Systems Based on the Merged Process of Petri Nets

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.