Verification of Hierarchical Artifact Systems
| Autor: | Yuliang Li, Alin Deutsch, Victor Vianu |
|---|---|
| Přispěvatelé: | Department of Computer Science and Engineering [San Diego] (CSE-UCSD), University of California [San Diego] (UC San Diego), University of California-University of California, Verification in databases (DAHU), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), NSF, ACM, Dahu, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), University of California (UC)-University of California (UC) |
| Rok vydání: | 2016 |
| Předmět: |
FOS: Computer and information sciences
Hierarchy [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB] Theoretical computer science Computer science Concurrency tem- poral logic Databases (cs.DB) Context (language use) business process management 02 engineering and technology Artifact (software development) Static analysis Computer Science - Databases 020204 information systems Quantifier elimination data-centric workflows 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing IBM verification Information Systems Foreign key |
| Zdroj: | Proceedings of the 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016) 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016) 35th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2016), Jun 2016, San Francisco, United States. pp.179-194, ⟨10.1145/2902251.2902275⟩ |
| DOI: | 10.1145/2902251.2902275 |
| Popis: | 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 decidability 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. Full version of the accepted PODS paper |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|