Efficiency of formal verification of ArchiMate business processes with NuSMV model checker
Piotr Szwed
DOI: http://dx.doi.org/10.15439/2015F44
Citation: Proceedings of the 2015 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 5, pages 1427–1436 (2015)
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.