Data-aware Workflow Modeling And Verification

Workflow modeling formally and verification is a significant link in workflow lifecycle. Data is an important component in business process. Current modeling languagesof business process support to model data based on control flow perspective. However,there are still great challenges on formally modeling data perspective in workflow, furtherthe formal verification of workflow with data is influenced in building time. The thesisextends workflow nets with workflow relevant data and application data on workflowmodeling. Based on modeling workflow taking into account data perspective, the thesisgives solutions for the two open problems of analyzing process models with soundnessproperty and consistency property. The key contributions of the thesis are as follows:The issue of data-aware workflow modeling was studied in detail. We have definedworkflow net with the aware of relevant data and application data. For the aware ofrelevant data aspect, conditions as well as data writing operations are assigned ontransitions, in addition, condition is formally defined from both a syntactic and asemantic point of view. For the aware of application data aspect, object operationsand object-state-pairs are taken into on tasks in the process model. Also, the objectbehaviour model was given.The issue of soundness of workflow taking into account data perspective was stud-ied in detail. We have given the behavior semantics of DWF-nets with the influenceof transition condition in detail. Then we have presented an approach to verify theworkflow correctness based on symbolic reachability analysis and have proposedsome methods to solve the state space problems.The issue of consistency between workflows and object lifecycles in informationsystems was studied in detail. Syntactical requirements for such consistency wereformalised as well as semantical requirements, i.e. requirements that ensure desir-able runtime behaviour. It was formally demonstrated that the problem of determin-ing behavioural consistency can be solved through a transformation to WF-nets andusing an established and already implemented approach to determining soundnessof these nets. The approaches mentioned above were implemented as plug-ins of the frameworkfor process analysis named ProM. For DWF-net soundness analysis, this plug-in was usedto test soundness of a number of real-life models. The application of the plug-in to thesemodels shows that our approach was able to correctly assess the correctness of processdefinition with a concrete data refinement. For DWF-net consistency analysis, both thesyntactical and semantical requirements served as the basis for an analysis plug-in thatwas developed for the ProM framework. This plug-in was used to test properties of anumber of real-life models. The application of the plug-in to these models showed thepresence of a number of syntactical and semantical errors. An empirical evaluation ofthe tool was also performed with industrial partners using the well-known questionnaire-based method. The evaluation and feedback from practitioners further evidenced thepractical significance of this research issue in the PLM field and demonstrated that theproposed solution with its automated tool support possessed a high application potential.