Informatica

Business Process Model and Notation (BPMN) is the leading visual notation used for modelling business processes. This paper shows how the Alvis modelling language can be used for formal analysis of BPMN models. Alvis supports graphical modelling of interconnections among subsystems called agents as well as a high-level programming specification for describing the agents’ behaviour. Its advantage is the possibility of formal verification using proven model checking techniques. We propose a translation from the BPMN model to the Alvis representation, which is discussed and evaluated using an illustrative example of a process for evaluation of a student assignment. Thanks to the translation it is possible to perform formal verification of a BPMN model in a high-level concurrent environment. As opposed to some low-level representations, such as Petri nets, semantics of Alvis is close to the original BPMN model. Moreover, if a concurrent system behaviour is specified using a BPMN model, it is possible to generate a formal model (a preliminary implementation) of the system.