Formal Semantics of BPMN Process Models Using YAWL

The Business Process Modeling Notation (BPMN) is an emerging standard for capturing business processes. However, BPMN lacks a formal semantics and many of its features are subject to interpretation, which is hindered the BPMN as a standard to statically check the semantic correctness of models. The fact that BPMN integrates constructs from graph-oriented process definition languages with features for macro of advanced constructs and the transmission of messages between two participants, make it challenging to provide a formal semantics of BPMN. Even more define a semantic that can be used to analyst BPMN models. This paper proposes a formal semantics of BPMN defined in terms of a mapping to YAWL nets, for which efficient analysis techniques exists. The proposed mapping has been implemented as a tool that generates code in the ProM.