Formal techniques for analyzing business process models

Scope and purpose of study. A business process is an ordered sequence of tasks involving people, materials, equipment, and information, designed to achieve some specific outcome. Well-designed business processes exploit the power of concurrency, and the flexibility of choice and asynchronous control; however, combining concurrency and choice could lead to incorrect process designs. The purpose of this dissertation is to develop techniques for verifying the correctness of a process's design. This is particularly relevant to the growing interest in process automation, where automated control and coordination of a business process requires that the process, by design, be correct.; The design of a business process minimally requires the specification of the process's logic, and the resource requirements for the various tasks. Business processes arise in numerous contexts; however, the design verification issues are the same, namely, (i) does the flow of control, i.e., process logic, ensure that the process will execute correctly from initiation to completion, and (ii) is the release and capture of shared resources among different tasks, either in the same, or in different instances of the process, well-designed so as to avoid deadlock? These are the questions dealt with, in this dissertation.; Research contributions. This dissertation presents a comprehensive foundation for the formalization and verification of business process designs. The specific contributions of this dissertation are: (1) Control Flow Verification: A recursive, backtracking algorithm for verifying the correctness of a process's logic has been developed. The algorithm does not impose any restrictions on the form/structure of the model, and also provides precise diagnostic feedback about the reasons for the control flow error(s), if any. (2) Resource-sharing Correctness: A novel Petri-net theoretic approach has been developed to (i) compute the minimal resource requirements that guarantee the successful execution of the process, and (ii) alert the designer about potential deadlock possibilities that may arise either within a single-, or across multiple-instances of the process.; The algorithms developed in this dissertation have been implemented in a comprehensive computerized environment called MAPS—M&barbelow;odeling and A&barbelow;nalysis of business P&barbelow;rocess modelS&barbelow;. Ideally, MAPS should grow as a research test-bed for new ideas and algorithms in business process modeling.