Verification of Semantically-Enhanced Artifact Systems (Extended
  Version)
  Artifact-Centric systems have emerged in the last years as a suitable
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.
