A Methodology for Automatic Formal Verification of Enterprise Architecture

International Journal of Information System Modeling and Design. 2019. Vol. 10. No. 1. P. 1–19.

Babkin E., Malyzhenkov P. V., Ivanova M., Ponomarev N.

For over a decade IT-business alignment has been ranked as a top-priority management concern, but there is little research on practical ways to achieve the alignment. EA development is a continuous iterative process, which implicitly ensures the achievement of a specific IT-business alignment level. Therefore, it is necessary to formalize the requirements for architecture and be able to automatically verify them. We propose a new methodology for detecting logical contradictions in enterprise architecture models based on a model checking approach adopted in the context of business modeling. In such methodology we use ArchiMate standard for a conceptual enterprise architecture description language which is fully aligned with TOGAF. We also offer several important verification queries and demonstrate practical applicability of our approach using a software prototype of the modeling tool which exploits MIT Alloy Analyzer model checking framework integrated with AchiMate Archi workbench.

Keywords: verification, enterprise architecture, Archi, SAM, IT-business alignment, TOGAF, Alloy Analyzer, ArchiMate, consistency analysis