使用约束Horn子句验证时间感知业务流程
计算机科学中的逻辑
2016-08-10 v1 软件工程
摘要
我们提出了一种验证时间感知业务流程属性的方法，即那些明确考虑了活动时间约束的业务流程。业务流程使用业务流程建模符号（BPMN）的扩展来指定，持续时间由整数上的约束定义。操作语义的定义由一组约束Horn子句（CHC）OpSem给出。我们的验证方法包括两个步骤。（步骤1）我们针对给定的业务流程和待验证的给定时间属性对OpSem进行特化，从而得到一组CHC，其可满足性等价于给定属性的有效性。（步骤2）我们使用最先进的CHC求解器来检查这些子句集的可满足性。我们已使用VeriMAP转换系统以及用于CHC的Eldarica和Z3求解器实现了我们的验证方法。
引用
@article{arxiv.1608.02807,
title = {Verification of Time-Aware Business Processes using Constrained Horn Clauses},
author = {Emanuele De Angelis and Fabio Fioravanti and Maria Chiara Meo and Alberto Pettorossi and Maurizio Proietti},
journal= {arXiv preprint arXiv:1608.02807},
year = {2016}
}
备注
Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)