Skip to Main content Skip to Navigation
New interface
Conference papers

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
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Gwen Salaün Connect in order to contact the contributor
Submitted on : Monday, September 3, 2018 - 11:10:30 AM
Last modification on : Wednesday, July 6, 2022 - 4:13:26 AM
Long-term archiving on: : Tuesday, December 4, 2018 - 3:45:23 PM


Files produced by the author(s)


  • HAL Id : hal-01866268, version 1


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⟩



Record views


Files downloads