F.: Verification of deployed artifact systems via data abstraction

Abstract. Artifact systems are a novel paradigm for specifying and implement-ing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycle models, accounting for the relational struc-ture of the artifact state and its possible evolutions over time. We consider the problem of verifying artifact systems against specifications expressed in quan-tified temporal logic. This problem is in general undecidable. However, when artifact systems are deployed, their states can contain only a bounded number of elements. We exploit this fact to develop an abstraction technique that enables us to verify deployed artifact systems by model checking their bounded abstraction.