Formalisation of BPMN Models: a Focus on Correctness Properties

The BPMN standard has a huge uptake in modelling business processes within the same organisation or involving multiple ones. Its primary goal is to create a standardised bridge for the gap between process design and process implementation in order to entirely automate the business process management lifecycle. In this context, the BPMN lack of a precise semantics represents a big issue, since it can lead to different interpretations, and hence implementations, of its features. Thus, providing a formal semantics of the BPMN notation is crucial for shaping IT systems and guaranteeing that these systems behave as they are supposed to do. On the one hand a formal semantics allows to overcome misunderstandings due to the use of natural language in the standard; on the other hand it enables the study of model properties, paving the way for correctness verification. This is indeed a clearly perceived need, as business process models, while primarily intended for process documentation and communication, are nowadays often also used as input for developing process-aware information systems and service-oriented applications. High quality of business process models is important for all these goals and correctness is an important indicator of it. Its relevance is also highlighted by the observation that incorrect models can lead to wrong decisions regarding a process and to unsatisfactory implementations of information systems. Tackling the above issues, this thesis contributes to the definition of a direct BPMN operational semantics, providing a uniform formal framework to study BPMN models and their main correctness properties. The formalisation allows to formally characterise important properties in the business process modelling domain, namely well-structuredness, safeness and soundness, thus classifying BPMN models according to the properties they satisfy. This leads to achieve advances in classifying BPMN models, by directly addressing BPMN models and their specificities. Concerning the formalisation, first a formal semantics for a core subset of BPMN elements is provided and then it is extended, by including other elements and business perspectives. Specifically, are considered features widely recognised as tricky and challenging to be formalised such as the OR-Join gateway, the sub-process element and multiple interacting participants, who exchange messages and data, in order to check if the obtained results are still valid in an extended framework.