Recent years have witnessed the evolution of business process specification frameworks from the traditional process-centric approach towards data-awareness. Process-centric formalisms focus on control flow while under-specifying the underlying data and its manipulations by the process tasks, often abstracting them away completely. In contrast, data-aware formalisms treat data as first-class citizens. The presence of data implies an increase expressiveness of business process specification, including often data dependencies and arithmetic. This thesis studies the verification problem of temporal properties on data-aware business specifications with data dependencies and arithmetic.
In our context, data implies infinite-state systems, for which verification is notoriously difficult. Unlike previous work, we focus on verification that is (a) automatic (i.e. no expert user is required to help the process of verification as for theorem provers), (b) sound and complete, and (c) does not abstract away the data portion, retaining the ability to check the effects of data values on the behavior of the process (e.g. in a prototypical e-commerce business process, abstracting the data would make it impossible to check if the payment received for a product matches the price reported on the bill).
We identify a practically significant class of business process specifications with data dependencies and arithmetic, for which verification of temporal properties is decidable. Besides decidability, in the context of commonly occurring classes of specifications, we develop verification techniques with upper bounds palatable to implementation, e.g. PSPACE for a common class of specifications with unary keys and fixed-arity databases with acyclic foreign keys.
We implement a verifier prototype based on our theoretical results and measure the running times of the verification of temporal properties on a wide range of business process specifications of different complexities. Our random generation is based on patterns and frequencies found in real-world business process specifications and properties. The average running times measured range from seconds to minutes for the more complex specifications.
We argue that the work in this thesis proves the feasibility of automatic verification of temporal properties on highly expressive business process specifications, that is both sound and complete.
|Advisor:||Deutsch, Alin B., Vianu, Victor|
|Commitee:||Hull, Richard, Ludaescher, Bertram, Papakonstantinou, Yannis, Remmel, Jeffrey|
|School:||University of California, San Diego|
|Department:||Computer Science and Engineering|
|School Location:||United States -- California|
|Source:||DAI-B 73/01, Dissertation Abstracts International|
|Keywords:||Arithmetic, Business processes, Feedback-freedom, Verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be