From Process Models to Concurrent Systems in Alvis Language

Article type: Research Article

Authors: Szpyrka, Marcin^{; *} | Nalepa, Grzegorz J. | Kluza, Krzysztof

Affiliations: AGH University of Science and Technology, Department of Applied Computer Science, al. A. Mickiewicza 30, 30-059 Krakow, Poland, E-mails: mszpyrka@agh.edu.pl, gjn@agh.edu.pl, kluza@agh.edu.pl

Correspondence: [*] Corresponding author.

Abstract: 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.

Keywords: business process model verification, Alvis modelling language, concurrent model, formal verification, Business Process Model and Notation (BPMN)

Journal: Informatica, vol. 28, no. 3, pp. 525-545, 2017