Quality Assurance for Business Process Models: a Focus on Understandability and Correctness

Business processes and their management are nowadays receiving more and more attention, in academia, industry and public administration sectors. They consist of sets of activities carried out to reach a specific goal (i.e. delivering a product or a service). The representation of those processes by means of graphical models is a widely used practice which allows for having a clear picture of the overall actions and interactions that should occur. Those models, once designed, can be used to guarantee qualities of the business processes they represent. In fact, specific verifications can be carried out on top of those models to evaluate, for example, properties such as understandability, and correctness which are considered indicators of high quality business processes. A scenario where understandability of business process models is crucial is the one of the LearnPAd project. LearnPAd uses business process models for sharing knowledge of the public administration processes across public servants, so techniques to guarantee model understandability are required. Some business process modeling practices can be adopted to foster the design of understandable models. However, an incorrect model, even if it is considered understandable, it cannot be of practical use if it leads to execution problems. Then, also techniques to verify business process model correctness are required. In this thesis, I present an overview of how the issue of assuring business process qualities is tackled in the literature, with a specific focus on understandability and correctness. Concerning understandability, my contribution relies on a collection of 50 BPMN modeling guidelines extracted from the literature and provided in a template that may enhance their usability. The work on understandability concluded with the development of a tool named BEBoP which allows the automatic verification of understandability modeling guidelines over BPMN models. Concerning model correctness, I contributed to the definition of a BPMN Operational Semantics, and to its implementation in the Maude system which enables verification by applying model checking techniques. The work on correctness concluded with the development of a tool called BProVe which allows to verify correctness properties, such as soundness and safeness, of business process models represented by means of the BPMN notation. All the developed tools have been tested over a set of thousands of BPMN models coming from the Academic Initiative repository. This allowed to verify their efficiency and usability in practice, and to provide statistics and considerations about those business process models. Many of the analyzed models violated both understandability and correctness properties. This is a clear evidence that proves the need for tools that can help model designers in designing understandable and correct models.