Analysis of the consistency of enterprise architecture models using formal verification methods

Abstract

Enterprise architecture design is a complex process which makes it possible to synchronize the capabilities and needs of business and information technologies (IT). It can be achieved by clarifying the understanding and formalization of the business processes and the interaction of the elements of the system through their formal description. The large number of interacting business processes and enterprise architecture entities raises the question of verifying their correctness. Therefore, it is necessary to formalize the requirements for architecture and be able to automatically verify them. In this paper, we propose a method for detecting logical contradictions in enterprise architecture models based on a model checking approach adopted in the context of business modeling. As an enterprise architecture description language, we use the modern open and independent ArchiMate standard. Developed by The Open Group, the standard provides a general specification for business processes, organizational structures, information flows, IT-systems and the technical infrastructure description of the enterprise. As a verifier, the language and tools of the MIT Alloy Analyzer system were chosen; they facilitate analysis of model constraints in terms of relational logic by automatically generating structures that satisfy the requirements of a logical model. In this paper, we propose to simplify and automate the process of specification and verification of enterprise architecture domain models using Archi - the visual editor for ArchiMate models. We have developed the editor plug-in which translates the enterprise architecture models into the language of the MIT Alloy Analyzer system and uses the meta-model of the ArchiMate specification as the basis for constructing specific domain models. The proposed method and software solutions have been tested using the ArciSurance case and their enterprise architecture model.