Artifact Systems With Data Dependencies and Arithmetic
The authors revisit the static verification problem for data centric business processes, specified in a variant of IBM's "Business artifact" model. Artifacts are records of variables that correspond to business-relevant objects and are updated by a set of services equipped with pre-and-post conditions, that implement business process tasks. The verification problem consists in statically checking whether all runs of an artifact system satisfy desirable properties expressed in a firstorder extension of linear-time temporal logic. In previous work, they identified the class of guarded artifact systems and properties, for which verification is decidable.