Verification of Artifact-Centric Systems: Decidability and Modeling Issues

TL;DR

This paper investigates the decidability of verifying artifact-centric systems, specifically GSM models, by translating them into a formal framework and identifying conditions under which verification becomes decidable.

Contribution

It introduces a translation of GSM models into a formal framework and proposes guidelines to ensure models are state-bounded and verifiable.

Findings

Verification of GSM is undecidable in general.

A class of state-bounded GSM models allows for decidable verification.

Guidelines are provided to transform GSM models into verifiable forms.

Abstract

Artifact-centric business processes have recently emerged as an approach in which processes are centred around the evolution of business entities, called artifacts, giving equal importance to control-flow and data. The recent Guard-State-Milestone (GSM) approach provides means for specifying business artifacts lifecycles in a declarative manner, using constructs that match how executive-level stakeholders think about their business. However, it turns out that formal verification of GSM is undecidable even for very simple propositional temporal properties. We attack this challenging problem by translating GSM into a well-studied formal framework. We exploit this translation to isolate an interesting class of state-bounded GSM models for which verification of sophisticated temporal properties is decidable. We then introduce some guidelines to turn an arbitrary GSM model into a state-bounded, verifiable model.