Automatic Verification of Data-Centric Business Processes

We formalize and study business process systems that are centered around "business artifacts", or simply "artifacts". Artifacts are used to represent (real or conceptual) key business entities, including both their data schema and lifecycles. The lifecycle of an artifact type specifies the possible sequencings of services that can be applied to an artifact of this type as it progresses through the business process. The artifact-centric approach was introduced by IBM, and has been used to achieve substantial savings when performing business transformations. In this paper, artifacts carry attribute records and internal state relations (holding sets of tuples) that services can consult and update. In addition, services can access an underlying database and can introduce new values from an infinite domain, thus modeling external inputs or partially specified processes described by pre-and-post conditions. The lifecycles associate services to the artifacts using declarative, condition-action style rules. We consider the problem of statically verifying whether all runs of an artifact system satisfy desirable correctness properties expressed in a first-order extension of linear-time temporal logic. We map the boundaries of decidability for the verification problem and provide its complexity. The technical challenge to static verification stems from the presence of data from an infinite domain, yielding an infinite-state system. While much work has been done lately in the verification community on model checking specialized classes of infinite-state systems, the available results do not transfer to our framework, and this remains a difficult problem. We identify an expressive class of artifact systems for which verification is nonetheless decidable. The complexity of verification is PSPACE-complete, which is no worse than classical finite-state model checking. This investigation builds upon previous work on verification of data-driven Web services and ASM transducers, while addressing significant new technical challenges raised by the artifact model. Copyright 2009 ACM.