TY - GEN
T1 - Symbolic specification and verification of data-aware BPMN processes using rewriting modulo SMT
AU - Durán, Francisco
AU - Rocha, Camilo
AU - Salaün, Gwen
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018
Y1 - 2018
N2 - 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 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.
AB - 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 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.
UR - http://www.scopus.com/inward/record.url?scp=85053937313&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-99840-4_5
DO - 10.1007/978-3-319-99840-4_5
M3 - Conference contribution
AN - SCOPUS:85053937313
SN - 9783319998398
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 76
EP - 97
BT - Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings
A2 - Rusu, Vlad
PB - Springer Verlag
T2 - 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018
Y2 - 14 June 2018 through 15 June 2018
ER -