Matrix Representation and Automation for the Verification of Free-Choiceness in Robustness Diagram with Loop and Time Controls
摘要
Workflow models aid in effective system representation and help in the assessment and improvement of various system qualities defined over some structural or behavioral aspects of their model properties. This research focuses on a multidimensional workflow, called the Robustness Diagram with Loop and Time Controls (or RDLT), and its free-choice property for such system representation and model verification. Free-choiceness is critical to induce behaviors like race condition avoidance. To date, there is still no supporting algebraic representations and automation tools for an efficient verification of free-choiceness of RDLTs. To address this gap, this paper presents a matrix-based representation for RDLTs and using this approach for automated verification of checking free-choiceness in RDLTs, focusing on the \(\varSigma \) -distinct Parent-Child Structure (PCS) configuration. In particular, this research employs a two-step verification phase focusing on structural analysis of related components and their adjacencies and constraint matrices. Thereafter, it evaluates their shared neighborhood and simultaneous reachability. Both phases are supported by a set of formally proven lemmas and theorems, ensuring the correctness of the verification process. Finally, we provide an automation tool to efficiently verify such RDLT free-choiceness and report our experimental results. Overall, this work contributes toward improving efficiency and reducing manual errors in analyzing complex workflow models.