UC San Diego

Data-driven workflows, of which IBM's Business Artifacts are a prime exponent, have been successfully deployed in practice, adopted in industrial standards, and have spawned a rich body of research in academia, focused primarily on static analysis. This thesis represents a significant advance on the problem of verifying data-driven workflows in two major aspects.

First, this thesis introduces Hierarchical Artifact Systems (HAS), a much richer and more realistic model than in previous work incorporating core elements of IBM's successful Guard-Stage-Milestone model. In particular, the HAS model features task hierarchy, concurrency, and richer artifact data. It also allows database key and foreign key dependencies, as well as arithmetic constraints. The results show decidability of verification and establish its complexity under a set of reasonable restrictions, making use of novel techniques including a hierarchy of Vector Addition Systems and a variant of quantifier elimination tailored to this context.

Second, this thesis bridges the gap between the theory and practice of data-driven workflow verification with two successful implementations, SpinArt and VERIFAS. SpinArt is a practical verifier based on the classical model-checking tool Spin which can verify a core subset of the HAS model. The implementation includes nontrivial optimizations and achieves good performance on real-world business process examples. VERIFAS further bridges the gap with a specialized implementation built from scratch.It verifies within seconds linear-time temporal properties over both real-world and synthetic workflows of complexity in the range recommended by software engineering practice. Compared to SpinArt, VERIFAS not only supports a model with richer data manipulations but also outperforms it by over an order of magnitude. VERIFAS' good performance is due to a novel symbolic representation approach and a family of specialized optimizations. To the best of our knowledge, these implementations are the first implementations of practical significance of artifact verifiers with full support for unbounded data.