Business process modeling using Petri nets

Business process modeling has become a standard activity in many organizations. We start with going back into the history and explain why this activity appeared and became of such importance for organizations to achieve their business targets. We discuss the context in which business process modeling takes place and give a comprehensive overview of the techniques used in modeling. We consider bottom up and top down approaches to modeling, also in the context of developing correct-by-construction models of business processes. The correctness property we focus on is soundness, or weak termination, basically meaning that at every moment of its execution, a process has an option to continue along an execution path leading to termination, which is an important sanity check for business processes. Finally, we discuss analogies between business processes and software services and their orchestrations and argue the applicability of the described modeling techniques to the world of services.