A visual token-based formalization of BPMN 2.0 based on in-place transformations

Context siness Process Model and Notation (BPMN) standard informally defines a precise execution semantics. It defines how process instances should be updated in a model during execution. Existing formalizations of the standard are incomplete and rely on mappings to other languages. ive aper provides a BPMN 2.0 semantics formalization that is more complete and intuitive than existing formalizations. rmalization consists of in-place graph transformation rules that are documented visually using BPMN syntax. In-place transformations update models directly and do not require mappings to other languages. We have used a mature tool and test-suite to develop a reference implementation of all rules. s rmalization is a promising complement to the standard, in particular because all rules have been extensively verified and because conceptual validation is facilitated (the informal semantics also describes in-place updates). sion our formalization has already revealed problems with the standard and since the BPMN is still evolving, the maintainers of the standard can benefit from our results. Moreover, tool vendors can use our formalization and reference implementation for verifying conformance to the standard.