Declarative business process models, notably Dynamic Condition Response (DCR) graphs, have gained traction as an alternative to traditional imperative approaches. However, adequate verification tools for such models remain scarce. This paper proposes a model-checking approach for DCR graphs verification using Coloured Petri Nets (CPN) as a pivot language. The transformation from DCR to CPN is proven to preserve semantics, ensuring the resulting model aligns with the original. Once transformed, the CPN model can be checked by any model checker to verify specific properties. We have automated this process via a C++ prototype that generates CPNs in the specification language of Helena, the model checker that we choose to leverage in our work.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formal Verification of Declarative Specifications of BPs: DCR2CPN-Based Approach

  • Ikram Garfatta,
  • Kaïs Klai,
  • Walid Gaaloul

摘要

Declarative business process models, notably Dynamic Condition Response (DCR) graphs, have gained traction as an alternative to traditional imperative approaches. However, adequate verification tools for such models remain scarce. This paper proposes a model-checking approach for DCR graphs verification using Coloured Petri Nets (CPN) as a pivot language. The transformation from DCR to CPN is proven to preserve semantics, ensuring the resulting model aligns with the original. Once transformed, the CPN model can be checked by any model checker to verify specific properties. We have automated this process via a C++ prototype that generates CPNs in the specification language of Helena, the model checker that we choose to leverage in our work.