Data-Centric Business Processes: Specification and Static Analysis
· Elio Damaggio (UCSD PhD student)
· Richard Hull (IBM TJ Watson Research)
Businesses and other organizations increasingly rely on business process management, and in particular the management of electronic workflows underlying business processes. These workflows are often centered around a database. They are typically very complex and prone to costly bugs, which leads to a critical need for computer-aided design and static analysis tools. Such tools would result in enhanced functionality, as well as increased confidence in the robustness and correctness of complex business processes. They would potentially benefit a wide variety of applications ranging from e-commerce to digital government to healthcare and scientific applications. Classical software verification techniques applicable to static analysis include model checking and theorem proving. However, both have serious limitations: Model checking requires finite-state abstraction, which results in serious loss of semantics or both the business process and verified properties. Theorem proving is incomplete and requires expert user feedback. This project proposes an alternative approach to static analysis. Instead of applying general-purpose techniques with only partial guarantees of success, it aims to identify restricted but sufficiently expressive classes of business processes for which sound and complete static analysis can be performed in a fully automatic way. Moreover, the target of verification consists of semantically rich data-aware workflows, in contrast to the traditional process-centric workflows. Data awareness is a feature of central importance in applications such as the above, which has recently led to the emergence of a new approach to workflow specification in which data is pre-eminent. This approach, introduced by IBM, focuses on data records, known as "business artifacts" or simply "artifacts", that correspond to key business-relevant objects, their life cycles, and the services (or tasks) that are invoked on the artifacts. IBM's artifact-centric approach has been demonstrated to yield substantial improvements to the operations of medium- and large-sized businesses.
The main objective of the present project is to develop new tools for the high-level specification and verification of such data-centric business processes.
The project investigates the trade-offs between the expressiveness of the specification language and the feasibility of the analysis tasks. It aims to establish tractability boundaries for static analysis and to develop practical algorithms and heuristics. Tools are to be developed for carrying out analysis tasks, that will be integrated with Siena, IBM's prototype for compiling artifact-centric business process specifications into workflow support code. The technical problems raised are intellectually quite challenging, and bring into play techniques from logic, automata theory, computational complexity, algorithms, and computer-aided verification. The resulting static analysis tools have high potential for becoming a transformational technology in the area of business processes.
Alin Deutsch , Richard Hull , Fabio Patrizi , Victor Vianu. Automatic Verification of Data-centric
Business Processes. International
Conference on Database Theory (ICDT) ,
Victor Vianu. Automatic verification of database-driven systems: a
new frontier. International
Conference on Database Theory (ICDT) ,
· Serge Abiteboul, Pierre Bourhis, Victor Vianu. Comparing the Expressiveness of Workflow Languages: A Matter of Views. International Conference on Database Theory (ICDT) , Uppsala, March 2011.
· Elio Damaggio, Alin Deutsch, Victor Vianu. Artifact Systems with Data Dependencies and Artithmetic Constraints. International Conference on Database Theory (ICDT) , Uppsala, March 2011.
· Elio Damaggio, Alin Deutsch, Dayou Zhou. Querying contract databases based on temporal behavior. ACM SIGMOD conference, June 2011.
· Richard Hull, Elio Damaggio, Riccardo De Masellis, Fabiana Fournier, Manmohan Gupta, Fenno Heath Iii, Stacy Hobson, Mark Linehan, Sridhar Maradugu, Anil Nigam, Piyawadee Sukaviriya, Roman Vaculin. Business Entities with Guard-Stage-Milestone Lifecycles: Managing Entity Interactions with Conditions and Events. ACM International Conference on Distributed Event-Based Systems (DEBS), 2011.
Elio Damaggio, Rick Hull, Roman Vaculin.
On the equivalence of
incremental and fixpoint semantics for business
entities with guard-stage-milestone lifecycles. International Conference on Business Process Management (BPM), 2011.