Symbolic Specification and Verification of Data-aware BPMN Processes using Rewriting Modulo SMT

Abstract : The Business Process Model and Notation (BPMN) is the standard notation for modeling business processes. It relies on a workflow-based language that allows for the modeling of the control-flow graph of an entire process. In this paper, the main focus is on an extension of BPMN with data, which is convenient for describing real-world processes involving complex behavior and data descriptions. By considering this level of expressiveness due to the new features, challenging questions arise regarding the choice of the semantic framework for specifying such an extension of BPMN, as well as how to carry out the symbolic simulation, validation, and assess the correctness of the process models. These issues are addressed first by providing a symbolic executable rewriting logic semantics of BPMN using the rewriting modulo SMT framework, where the execution is driven by rewriting modulo axioms and by querying SMT decision procedures for data conditions. Second, reachability properties, such as deadlock freedom and detection of unreachable states with data exhibiting certain values, can be specified and automatically checked with the help of Maude, thanks to its support for rewriting modulo SMT. The approach presented in this paper has been validated on realistic processes and it is illustrated with a running example.
Document type :
Conference papers
WRLA 2018 : 12th International Workshop on Rewriting Logic and its Applications, Apr 2018, Thessaloniki, Greece. pp.1-20
Liste complète des métadonnées

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01866268
Contributor : Gwen Salaün <>
Submitted on : Monday, September 3, 2018 - 11:10:30 AM
Last modification on : Thursday, October 11, 2018 - 8:48:04 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01866268, version 1

Collections

Citation

Francisco Durán, Camilo Rocha, Gwen Salaün. Symbolic Specification and Verification of Data-aware BPMN Processes using Rewriting Modulo SMT. WRLA 2018 : 12th International Workshop on Rewriting Logic and its Applications, Apr 2018, Thessaloniki, Greece. pp.1-20. 〈hal-01866268〉

Share

Metrics

Record views

62

Files downloads

25