This book provides the most complete formal specification of the semantics of the Business
Process Model and Notation 2.0 standard (BPMN) available to date in a style that is easily
understandable for a wide range of readers - not only for experts in formal methods but e.g.
also for developers of modeling tools software architects or graduate students specializing
in business process management.BPMN - issued by the Object Management Group - is a widely used
standard for business process modeling. However major drawbacks of BPMN include its limited
support for organizational modeling its only implicit expression of modalities and its lack
of integrated user interaction and data modeling. Further in many cases the syntactical and
in particular semantic definitions of BPMN are inaccurate incomplete or inconsistent. The
book addresses concrete issues concerning the execution semantics of business processes and
provides a formal definition of BPMN process diagrams which can serve as a sound basis for
further extensions i.e. in the form of horizontal refinements of the core language.To this
end the Abstract State Machine (ASMs) method is used to formalize the semantics of BPMN. ASMs
have demonstrated their value in various domains e.g. specifying the semantics of programming
or modeling languages verifying the specification of the Java Virtual Machine or formalizing
the ITIL change management process.This kind of improvement promotes more consistency in the
interpretation of comprehensive models as well as real exchangeability of models between
different tools. In the outlook at the end of the book the authors conclude with proposing
extensions that address actor modeling (including an intuitive way to denote permissions and
obligations) integration of user-centric views a refined communication concept and data
integration.
