Formal verification of declarative specifications of BPs: DCR2CPN-based approach

Overview & Synopsis

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.