SpinArt：一种基于自旋的并行系统验证器
SpinArt: A Spin-based Verifier for Artifact Systems
摘要：
数据驱动的工作流（IBM的Business Artifacts是其中的主要代表）已经成功地在实践中部署，在工业标准中采用，并在学术界产生了大量的研究，主要集中在静态分析上。在之前的工作中，我们获得了验证包含IBM成功的Guard-Stage-Milestone（GSM）工件模型核心元素的丰富模型的理论结果。结果表明，一个大类的GSM工作流的时间属性的验证的可判定性，并建立其复杂性。跟进这些结果，本文件报告的实施SpinArt，一个实际的验证的基础上，经典的模型检查工具自旋。该实现包括非平凡的优化，并在现实世界的业务流程示例中实现了良好的性能。我们的研究结果揭示了在数据驱动的工作流程的背景下，现成的验证器的能力和局限性。
英文摘要：
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. In previous work, we obtained theoretical results on the verification of a rich model incorporating core elements of IBM's successful Guard-Stage-Milestone (GSM) artifact model. The results showed decidability of verification of temporal properties of a large class of GSM workflows and established its complexity. Following up on these results, the present paper reports on the implementation of SpinArt, a practical verifier based on the classical model-checking tool Spin. The implementation includes nontrivial optimizations and achieves good performance on real-world business process examples. Our results shed light on the capabilities and limitations of off-the-shelf verifiers in the context of data-driven workflows.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
