Verification of GSM-based Artifact-centric Systems by Predicate Abstraction - Lomuscio,AR; griesmayer,A; gonzalez (Springer, 2015)
Artifact-centric systems are a recent paradigm to model and implementbusiness workflows. They describe data, processes, internal and external agents and include mechanisms for data hiding and access control. GSM is a language for the implementation of artifact-centric systems. Since GSM programs have infinitely many states, their verification is challenging. We here present a predicate abstraction technique that enables us to verify GSM programs against richspecifications built on an epistemic, first-order variant of the µ-calculus. We give the theoretical underpinnings of the technique and presentGSMC, the first model checker for GSM that implements SMT-based, three-valued abstraction for GSM.