多案例数据感知 BPMN 的形式化建模与基于 SMT 的参数化验证
计算机科学中的逻辑
2019-06-21 v3
摘要
我们提出 DAB——BPMN 事实标准的一种数据感知扩展，能够操作案例数据与持久数据（划分为只读目录与读写仓库），并在表达力与在其上支持安全性质参数化验证的可能性之间取得平衡。特别地，我们从构件系统验证的文献中汲取灵感，考虑这样一类验证问题：安全性质的检查独立于只读目录的内容，可能考虑无界数量的活跃案例以及目录与仓库中的元组。此类问题采用完全实现的基于数组的反向可达性技术来处理，该技术属于成熟的 SMT 模型检测传统。我们还识别出相关类的 DAB，对于它们，在 MCMT 基于数组的模型检测器中实现的反向可达性过程是可靠且完备的，并进一步强化了这些类以保证终止性。
引用
@article{arxiv.1905.12991,
title = {Formal Modeling and SMT-Based Parameterized Verification of Multi-Case Data-Aware BPMN},
author = {Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and Marco Montali and Andrey Rivkin},
journal= {arXiv preprint arXiv:1905.12991},
year = {2019}
}
备注
This article builds upon arXiv:1906.07811, extending it in two respects. First, while arXiv:1906.07811 focuses on the verification of DABs considering a single, running case, we consider here the possibility of (unboundedly many) cases running concurrently. Second, we provide full proofs of the technical results, including those from arXiv:1906.07811 and those for this version