An automation tool for model conversion and soundness verification from Robustness Diagrams with Loop and Time Controls to Petri Nets - Tongzon, Lyward Manuel S.; Malinao, Jasmine A. (Tacloban City Division of Natural Sciences and Mathematics, University of the Philippines Tacloban College, 2025)
This paper presents the development of an automated tool for converting Robustness Diagrams with Loop and Time Controls (RDLTs) into Petri Nets (PNs). The tool focuses primarily on preserving model correctness, structural fidelity, and soundness throughout the conversion process. We propose a graph-based approach for effectively mapping RDLT to PN using an existing algorithm from the literature [1]. This approach ensures that critical properties, such as traversal limits, time constraints, and reset-bound subsystems (RBS), 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, en-suring robust conversion for diverse RDLT configurations. A series of comprehensive tests were conducted to evaluate the tool's accuracy, performance, and reliability, with results contirining 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.
Undergraduate thesis (Bachelor of Science in Computer Science) -- University of the Philippines, Tacloban.
Includes bibliographical references.
Keywords: Software engineering