VERIFAS：面向制品系统的实用验证器
数据库
2017-09-29 v3 计算机科学中的逻辑
摘要
数据驱动工作流（IBM 的 Business Artifacts 是其典型代表）已在实践中成功部署，被工业标准采纳，并在学术界引发了以静态分析为主的丰富研究。本研究通过 VERIFAS 弥合了制品验证理论与实践之间的差距，VERIFAS 是首个具有实际意义的、完全支持无界数据的制品验证器实现。VERIFAS 能够在数秒内验证真实世界与合成工作流上的线性时序性质，这些工作流的复杂度处于软件工程实践所推荐的范围内。与我们先前基于广泛使用的 Spin 模型检测器的实现相比，VERIFAS 不仅支持具有更丰富数据操作的模型，而且在性能上超越其一个数量级以上。VERIFAS 的良好性能得益于一种新颖的符号表示方法和一系列专用优化技术。
引用
@article{arxiv.1705.10007,
title = {VERIFAS: A Practical Verifier for Artifact Systems},
author = {Yuliang Li and Alin Deutsch and Victor Vianu},
journal= {arXiv preprint arXiv:1705.10007},
year = {2017}
}
备注
arXiv admin note: text overlap with arXiv:1705.09427