An Automation Tool for Model Conversion and Soundness Verification from Robustness Diagrams with Loop and Time Controls to Petri Nets
摘要
This paper presents the development of a graph-based automation tool for converting Robustness Diagram with Loop and Time Controls (RDLT) into a Petri Net (PN) as inspired by a mapping in literature. This tool focuses primarily on preserving model correctness, structural fidelity, and various notions of workflow soundness throughout the conversion process. This approach ensures that critical properties of RDLTs, such as traversal limits, time constraints, and their reset-bound subsystems, are accurately preserved. The system is equipped with an intuitive Graphical User Interface, allowing users to upload RDLT models, automatically generate the corresponding PNs, and perform soundness verification and firing sequence simulations. The tool’s modular design enables efficient handling of various model structures, including split nodes, reset arcs, and abstract edges, ensuring robust conversion for diverse RDLT configurations. A series of comprehensive tests were conducted to evaluate the tool’s accuracy, performance, and reliability, with results confirming its capability to produce valid PN models while ensuring soundness preservation. This research makes a significant contribution to the automation of RDLT-to-PN conversion, along with the verification of classical and relaxed soundness preservation. This approach effectively reduces manual effort and mitigates the potential for human error in workflow modeling.