• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

A Methodology for Automatic Formal Verification of Enterprise Architecture

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.