带恢复机制的业务工作流的 LTL 语义
软件工程
2014-06-06 v1 计算机科学中的逻辑
摘要
我们描述了一个包含异常行为管理（即恢复）的业务工作流案例研究，并展示了时序逻辑与模型检测如何提供一种方法论，以迭代修订设计并获得构造即正确的系统。为此，我们通过将通用工作流模式编译为 LTL 来定义形式语义，并利用有界模型检测器 Zot 证明特定属性与需求的有效性。我们的基本假设是，这种轻量级方法能轻松融入现有流程，而无需彻底改变程序、工具及人员态度。形式化的复杂性与方法的侵入性已被证明是将形式化工程技术部署到常规项目中的主要缺陷与障碍。
引用
@article{arxiv.1406.1395,
title = {An LTL Semantics of Business Workflows with Recovery},
author = {Luca Ferrucci and Marcello M. Bersani and Manuel Mazzara},
journal= {arXiv preprint arXiv:1406.1395},
year = {2014}
}