Verification of Semantically-Enhanced Artifact Systems (Extended Version)

Technical Report, arXiv.org e-Print archive. CoRR Technical Report arXiv:1308.6292 2013. Available at https://arxiv.org/abs/1308.6292.

Artifact-Centric systems have emerged in the last years as a sui table framework to model business-relevant entities, by combining their static and dynamic aspects. In particular, the Guard-Stage-Milestone (GSM) approach has been recently proposed to model artifacts and their lifecycle in a declarative way. In this paper, we enhance GSM with a Semantic Layer, constituted by a full-fledged OWL 2 QL ontology linked to the artifact information models through mapping specifications. The ontology provides a conceptual view of the domain under study, and allows one to understand the evolution of the artifact system at a higher level of abstraction. In this setting, we present a technique to specify temporal properties expressed over the Semantic Layer, and verify them according to the evolution in the underlying GSM model. This technique has been implemented in a tool that exploits state-of-the-art ontology-based data access technologies to manipulate the temporal properties according to the ontology and the mappings, and that relies on the GSMC model checker for verification.

@techreport{Corr-2013-gsm-semlayer,
   title = "Verification of Semantically-Enhanced Artifact Systems (Extended
Version)",
   year = "2013",
   author = "Bagheri Hariri, Babak and Diego Calvanese and Marco Montali
and Ario Santoso and Dmitry Solomakhin",
   institution = "arXiv.org e-Print archive",
   number = "arXiv:1308.6292",
   note = "Available at https://arxiv.org/abs/1308.6292",
}