Evaluating efficiency of archimate business processes verification with NuSMV

Abstract

The motivation for our work was an idea of integrating formal verification with business processes modeling. In the presented approach ArchiMate was selected as a language used for definition of processes. We describe a procedure, which extracts behavioral elements from ArchiMate specification and transforms them into a corresponding representation used by NuSMV model checker. Then, we focus on time efficiency of the verification task. We give results of tests performed on a set of artificial process specifications, as well as on a complex business process, whose development was supported by the implemented solution. We compare three semantics of ArchiMate process definitions and discuss their influence on model complexity and verification time.