Bonus – Overview
In week three we present soundness properties and rules, how business process models can be checked for these properties. Using a mapping from BPMN process models to Petri nets, these properties can be formulated formally and verified using the set of reachable states of a business process model. The following figure shows an example Petri net.
As this provides a more academic understanding of analyzing process behavior, we cover it in a bonus module.
All lectures, self tests, and homeworks of the bonus module are voluntary. Students who participate in the homeworks can earn additional 15 points (that are not added to the maximum reachable score) and thereby boost their overall score. Students who decide not to take the bonus homework will therefore have no disadvantage.
The bonus module comprises the following topics. Since these topic fall into the line of analyzing the behavior of business processes, which is why we tagged the lectures and quizzes 3.5 through 3.7.
- Informal Petri Net Primer Petri nets are directed graphs to represent the behavior of dynamic systems. Their strong mathematical foundation qualifies them for checking formal properties of systems. The behavior of Petri nets is represented by tokens. From the initial token distribution, the set of reachable states can be computed for systems analysis.
- Mapping BPMN Process Models to Petri Nets
In order to formally verify soundness of business process models, they need to be transformed to Petri nets. Elements of BPMN, e.g., activities and gateways, are mapped to Petri net fragments that are then connected to represent the behavior of a business process formally. - Checking Soundness
Based on a transformation of BPMN to Petri nets, the reachability graph of a process is built and analyzed for soundness. For instance, it is examined if the final state can always be reached and whether all transitions can contribute to a process instance.
Organization
You can find several self tests, by which you can check your learning progress. There is no time limit or submission deadline for these tests and you receive direct feedback on your answers. You can even repeat them.
At the end of the week, you may to submit a homework. This homework is voluntary and students, who decide not to submit the homework will not loose any points. In contrast, you have the chance to earn additional points to achieve an overall score of 100% in case you did not get all points in the other homework or in the exam.
You should schedule 30-45 minutes for the homework assignment, which has a hard time limit of 60 minutes . Please be advised that this test can only be started ONCE (closing the browser does not stop the timer). In addition, the homework starts when you click on the start button on the homework page. So, only click on the button if you are willing to take the assignment. The achieved score in the homework contributes to your total score for this course. You will be informed about your results and a sample solution is published a day after submission deadline.
In case you have questions regarding the lectures, self tests, or assignments, please use the community forum. Often these questions can be answered by your fellow students. Members of the teaching team also read the questions in the forum and help whenever help is needed. We are looking forward to fruitful discussions.
Have fun and good luck with the bonus module!
Weekly Schedule
Please be aware of the following dates for this week.
- The homework needs to be submitted latest May 2nd , 2016, at 22:00 (10:00 pm) CET to receive additional points. Submission is already open; after consulting the lecture material (videos, slides, and reading material), you can start on the homework right away.
- The solution for this week's homework will be published on Tuesday, May 03 rd, 2016, at 10:00 (am) CET.
- The material for the next week, covering Basics of Business Process Modeling, will be made available on Saturday, November 30 th, 2016, at 10:00 (am) CET.
- All times are Central European Summer Time (UTC+2). Please check your local time zone. The remaining time until May 2nd, 2016, at 22:00 (10:00 pm) can be checked at the provided link.
Reading Material
- Chapter 4.2 of the book Business Process Management – Concepts, Languages, Architectures (discount of 20% for printed version and discount of 50% for electronic version applies for participants of this course) covers the background and theoretical foundations of Petri nets. Structural soundness and soundness of Petri nets is discussed in Sections 6.3 and 6.4.
- A detailed introduction to Petri nets can be found in Wolfgang Reisig: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies. Springer 2013
- The article "The Application of Petri Nets to Workflow Management" by Wil Van der Aalst introduces Petri nets for analyzing business processes.
- In his seminal article "Verification of workflow nets" Wil Van der Aalst introduces the notion of soundness.
- The mapping of BPMN to Petri nets is informally covered in "Petri Net Transformations for Business Processes – A Survey" by Lohmann et al. based on a comprehensive formalization of the mapping that has been introduced by Dijkman et al. in "Formal Semantics and Automated Analysis of BPMN Process Models".