Formal Modeling and SMT-Based Parameterized Verification of Data-Aware BPMN

Proc. of the 17th Int. Conf. on Business Process Management (BPM 2019). Volume 11675 of Lecture Notes in Computer Science. 2019.

We propose DAB -- a data-aware extension of BPMN where the process operates over case and persistent data (partitioned into a read-only database called catalog and a read-write database called repository). The model trades off between expressiveness and the possibility of supporting parameterized verification of safety properties on top of it. Specifically, taking inspiration from the literature on verification of artifact systems, we study verification problems where safety properties are checked irrespectively of the content of the read-only catalog, and accepting the potential presence of unboundedly many tuples in the catalog and repository. We tackle such problems using an array-based backward reachability procedure fully implemented in MCMT -- a state-of-the-art array-based SMT model checker. Notably, we prove that the procedure is sound and complete for checking safety of DABs, and single out additional conditions that guarantee its termination and, in turn, show decidability of checking safety.

@inproceedings{BPM-2019,
   title = "Formal Modeling and SMT-Based Parameterized Verification of
Data-Aware BPMN",
   year = "2019",
   author = "Diego Calvanese and Silvio Ghilardi and Alessandro Gianola and
Marco Montali and Andrey Rivkin",
   booktitle = "Proc. of the 17th Int. Conf. on Business Process Management
(BPM 2019)",
   pages = "157--175",
   volume = "11675",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-030-26619-6_12",
}