Szczegóły publikacji
Opis bibliograficzny
Efficiency of formal verification of ArchiMate business processes with NuSMV model checker / Piotr SZWED // W: FedCSIS : abstracts of the Federated Conference on Computer Science and Information Systems : September 13-16, 2015, Łódź, Poland. — [Piscataway : IEEE], [2015]. — W bazie Web of Science seria: ACSIS-Annals of Computer Science and Information Systems ; ISSN 2300-5963 ; vol. 5. — Opis częśc. wg okł. — ISBN: 978-8-3608-1066-8. — S. 101. — Publikacja dostępna w części: 13th Conference on Advanced information technologies for management. — Pełny tekst na dołączonym Dysku Flash. — S. 1437-1446. — Wymagania systemowe: Adobe Reader. — Bibliogr. s. 1445-1446, Abstr. — W bazie Web of Science zakres stron: 1427–1436
Autor
Słowa kluczowe
Dane bibliometryczne
| ID BaDAP | 92170 |
|---|---|
| Data dodania do BaDAP | 2015-09-18 |
| DOI | 10.15439/2015F44 |
| Rok publikacji | 2015 |
| Typ publikacji | materiały konferencyjne (aut.) |
| Otwarty dostęp |  |
| Konferencja | Federated Conference on Computer Science and Information Systems |
Abstract
We investigate an application of model checking techniques to automated verification of business processes expressed in ArchiMate language. As a verification tool the state of the art symbolic model checker NuSMV is used. The proposed approach consists in fully automated translation of behavioral elements embedded in ArchiMate models into a corresponding representation in NuSMV language and then verifying its properties specified in CTL. Since our goal is to build an interactive verification tool, we focus on time efficiency of the verification process. We report results of tests performed on artificial process models of various complexity, as well as on a real business process example. The results show, that the described approach can be applied successfully, however, verification of complex business process specifications may face the problem of state space explosion. In such a case, to make the verification feasible, various reductions and simplifications can be applied.
