A matrix representation for the verification of free-choiceness of Robustness Diagram with Loop and Time Controls - Gabitanan, Rugie C.
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 model verification. Free-choiceness is critical to induce behaviors like race condition avoidance. To date, there is still no supporting algebraic representations for an efficient verification of free-choiceness of RDLTs. To address this gap, this paper presents a matrix-based representation for RDLTs to aid in automating the verification of checking free-choiceness in RDLTs. In particular, this research employs verification focusing on structural analysis of related components and their adjacencies and constraint matrices for verifying E-distinct PCS free-choice. This also evaluates their shared neighborhood and simultaneous reachability of siblings for verifying to-step PCN free-choice. Both stages in the verification are supported by a set of formally proven lemmas and theorems, ensuring the correctness of the verification process. Overall, this work contributes toward improving efficiency and reducing manual errors in analyzing complex workflow models.