Due to its versatility and wide variety of constructs, BPMN (Business Process Model and Notation) is today the leading standard notation for creating visual models of business or organizational processes. It is a rich and expressive graphical language specially designed to provide a notation that is easily understood by all members of a company. Sometimes, however, this large number of controls and action nodes available can become a weakness since a given semantics can be represented in many ways, causing some ambiguity and raising the question of bisimilarity between two models. Today, it is universally recognized that formal methods are useful for the specification, design and verification of almost all systems, and essential for the most critical ones. On the other hand, the Business Process Execution Language for Web Services (BPEL) is an executable language structured in blocks, supported by many execution platforms, making it possible to specify the actions in the business processes with Web services. Since BPMN and BPEL share almost the same level of abstraction, we present in this article a formalization of the BPMN language through a mapping to BPEL, aiming to remove its ambiguities, to solve the complex modeling and interaction problems and open the door to many formal analysis such as model checking. We first formalize the BPEL language using the K framework, we then map the BPMN language to this formalized version of BPEL. The K Framework is a rewriting/reachability based framework enabling language developers to formally define all programming languages. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification tool sets, compilers, debuggers and other developer tools for it.
Type Checking Semantic Functions in ASDF