Verification of Hierarchical Artifact Systems

Alin Deutsch 1 Yuliang Li 1 Victor Vianu 2, 1
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : Data-driven workflows, of which IBM's Business Artifacts are a prime exponent, have been successfully deployed in practice, adopted in industrial standards, and have spawned a rich body of research in academia, focused primarily on static analysis. The present work represents a significant advance on the problem of artifact verification, by considering a much richer and more realistic model than in previous work, incorporating core elements of IBM's successful Guard-Stage-Milestone model. In particular, the model features task hierarchy, concurrency, and richer artifact data. It also allows database key and foreign key dependencies, as well as arithmetic constraints. The results show decidabil-ity of verification and establish its complexity, making use of novel techniques including a hierarchy of Vector Addition Systems and a variant of quantifier elimination tailored to our context.
Type de document :
Communication dans un congrès
ACM. 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016), Jun 2016, San Francisco, United States. Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016), pp.179 - 194, 2016, Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016). 〈10.1145/2902251.2902275〉
Liste complète des métadonnées

Littérature citée [49 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01389845
Contributeur : Victor Vianu <>
Soumis le : dimanche 30 octobre 2016 - 04:23:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Fichier

main.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Citation

Alin Deutsch, Yuliang Li, Victor Vianu. Verification of Hierarchical Artifact Systems. ACM. 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016), Jun 2016, San Francisco, United States. Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016), pp.179 - 194, 2016, Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016). 〈10.1145/2902251.2902275〉. 〈hal-01389845〉

Partager

Métriques

Consultations de la notice

137

Téléchargements de fichiers

67