SpinArt: A Spin-based Verifier for Artifact Systems

TL;DR

SpinArt is a practical verifier for artifact systems based on Spin, demonstrating effective verification of business workflows with real-world performance, building on theoretical decidability results.

Contribution

This paper introduces SpinArt, a new verifier for artifact systems that leverages Spin, with optimizations and practical performance on real-world examples.

Findings

Effective verification of business workflows demonstrated

Optimizations improve Spin's performance on artifact models

Capable of handling real-world data-driven process examples

Abstract

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. In previous work, we obtained theoretical results on the verification of a rich model incorporating core elements of IBM's successful Guard-Stage-Milestone (GSM) artifact model. The results showed decidability of verification of temporal properties of a large class of GSM workflows and established its complexity. Following up on these results, the present paper reports on the implementation of SpinArt, a practical verifier based on the classical model-checking tool Spin. The implementation includes nontrivial optimizations and achieves good performance on real-world business process examples. Our results shed light on the capabilities and limitations of off-the-shelf verifiers in the context of data-driven workflows.