论文标题
具有算术条件的数据感知过程的健全性
Soundness of Data-Aware Processes with Arithmetic Conditions
论文作者
论文摘要
数据感知过程代表并整合了单个模型中的结构和行为约束，因此在业务过程管理和信息系统工程中越来越多地研究。在此范围内，由于它们能够平衡简单性与表现力的能力，数据培养皿（DPN）的流行程度越来越高。数据和控制流的相互作用使得检查了此类模型的正确性，特别是众所周知的健全性，至关重要和挑战性的属性。先前检查DPN合理性的方法的主要缺点是，它们在处理现实世界中的混凝土应用时考虑了数据条件，而无需算术。在本文中，我们通过提供一个基础和操作框架来评估富含算术数据条件的DPN的声音，来攻击这一开放问题。该框架带有概念验证的实现，而不是依靠临时技术，而是采用了现成的SMT技术。该实现在文献中的示例集和从此类示例中构建的合成变体中进行了验证。
Data-aware processes represent and integrate structural and behavioural constraints in a single model, and are thus increasingly investigated in business process management and information systems engineering. In this spectrum, Data Petri nets (DPNs) have gained increasing popularity thanks to their ability to balance simplicity with expressiveness. The interplay of data and control-flow makes checking the correctness of such models, specifically the well-known property of soundness, crucial and challenging. A major shortcoming of previous approaches for checking soundness of DPNs is that they consider data conditions without arithmetic, an essential feature when dealing with real-world, concrete applications. In this paper, we attack this open problem by providing a foundational and operational framework for assessing soundness of DPNs enriched with arithmetic data conditions. The framework comes with a proof-of-concept implementation that, instead of relying on ad-hoc techniques, employs off-the-shelf established SMT technologies. The implementation is validated on a collection of examples from the literature, and on synthetic variants constructed from such examples.
