@inproceedings{46a315af95b74bc48fae36453fda2a9d,
title = "Formal Verification of Declarative Specifications of BPs: DCR2CPN-Based Approach",
abstract = "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.",
keywords = "Business Process Management, Coloured Petri Nets, DCR, Model Checking, Temporal properties",
author = "Ikram Garfatta and Ka{\"i}s Klai and Walid Gaaloul",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.; 17th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2024 ; Conference date: 16-10-2024 Through 18-10-2024",
year = "2025",
month = jan,
day = "1",
doi = "10.1007/978-3-031-85356-2\_3",
language = "English",
isbn = "9783031853555",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "32--46",
editor = "\{Ben Hedia\}, Belgacem and Mohamed Ghazel and Bruno Monsuez",
booktitle = "Verification and Evaluation of Computer and Communication Systems - 17th International Conference, VECoS 2024, Proceedings",
}