工件中心系统的验证：可判定性与建模问题
软件工程
2013-04-08 v1 计算机科学中的逻辑
摘要
工件中心业务流程最近成为一种方法，其中流程围绕业务实体（称为工件）的演化展开，同等重视控制流和数据。最近的Guard-State-Milestone (GSM)方法提供了一种声明式指定业务工件生命周期的方式，使用与高管级利益相关者思考其业务相匹配的构造。然而，事实证明，即使对于非常简单的命题时态性质，GSM的形式验证也是不可判定的。我们通过将GSM转换到一个经过充分研究的形式框架中来攻克这一难题。我们利用这种转换来隔离一类有趣的状态有界GSM模型，对于这些模型，复杂时态性质的验证是可判定的。然后，我们引入一些指导原则，将任意GSM模型转换为状态有界、可验证的模型。
引用
@article{arxiv.1304.1697,
title = {Verification of Artifact-Centric Systems: Decidability and Modeling Issues},
author = {Dmitry Solomakhin and Marco Montali and Sergio Tessaris and Riccardo De Masellis},
journal= {arXiv preprint arXiv:1304.1697},
year = {2013}
}
备注
artifact-centric systems, guard-stage-milestone, formal verification