Szczegóły publikacji
Opis bibliograficzny
From process models to concurrent systems in Alvis language / Marcin SZPYRKA, Grzegorz J. NALEPA, Krzysztof KLUZA // Informatica (Vilnius) ; ISSN 0868-4952. — 2017 — vol. 28 no. 3, s. 525–545. — Bibliogr. s. 542–544, Abstr.
Autorzy (3)
Słowa kluczowe
Dane bibliometryczne
| ID BaDAP | 109723 |
|---|---|
| Data dodania do BaDAP | 2017-12-13 |
| Tekst źródłowy | URL |
| DOI | 10.15388/Informatica.2017.143 |
| Rok publikacji | 2017 |
| Typ publikacji | artykuł w czasopiśmie |
| Otwarty dostęp |  |
| Czasopismo/seria | Informatica |
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.