SpinArt：一种基于 Spin 的 Artifact 系统验证器
数据库
2018-03-21 v3 形式语言与自动机理论
摘要
数据驱动的工作流，其中 IBM 的业务 Artifact 是典型代表，已在实践中成功部署，被工业标准采纳，并在学术界催生了丰富的研究，主要集中在静态分析方面。在先前的工作中，我们对一个融合了 IBM 成功的 Guard-Stage-Milestone (GSM) Artifact 模型核心元素的丰富模型进行了验证，并取得了理论成果。这些成果表明了对一大类 GSM 工作流的时序属性进行验证的可判定性，并确立了其复杂性。作为这些成果的后续，本文报告了 SpinArt 的实现，这是一个基于经典模型检验工具 Spin 的实用验证器。该实现包含非平凡的优化，并在真实世界的业务流程示例上取得了良好性能。我们的结果揭示了现成验证器在数据驱动工作流背景下的能力与局限。
引用
@article{arxiv.1705.09427,
title = {SpinArt: A Spin-based Verifier for Artifact Systems},
author = {Yuliang Li and Alin Deutsch and Victor Vianu},
journal= {arXiv preprint arXiv:1705.09427},
year = {2018}
}