Article Preview
Top1. Introduction
Information technology and information systems have evolved from its traditional use as an organization’s operations automation tool to a critical strategic resource influencing the business value created by the company. The strategic alignment of business and information technologies has consistently been reported as one of the key CIO concerns across various industries. According to The Global IT Trends Survey (2017) the alignment issue has held its position in the top three IT management concerns since 2007 along with business agility and business cost reduction (Figure 1).
Figure 1.
Top IT management concerns (based on the data provided in the Global IT trends survey)
The trend is caused by benefits alignment may provide as well as risks entailed by misalignment. IT-business alignment enables organization to enhance its flexibility and maximize return on IT investments, which, in turn, leads to increased profitability and sustainable competitive advantage (Cataldo, McQueen & Hardings, 2012; Chan, Sabherwal & Thatcher, 2016; Chen, Kazman, & Garg, 2005).
Enterprise Architecture, which is defined as a set of models and definitions describing the structure of an enterprise, its subsystems and relationships between them, helps managers to find the best strategies for organizational development with respect to the information systems. EA development is a continuous iterative process which implicitly ensures the achievement of a specific IT-business alignment level. Consequently, logical contradictions in the EA structure are inextricably linked to the misalignment of IT and business within an organization. Therefore, it is vital to ensure EA logic consistency by continuous elicitation and elimination of any contradictions along the process of EA elaboration.
However, there is a lack of practical opportunities to carry out “manual testing” of an EA model in accordance with previously formulated requirements and the major part of proposed methodologies are qualitative or questionnaire-based (Kearns & Lederer, 2000, Luftman, 2003).
In this paper we close the gap mentioned and propose, a methodology of EA formal verification for the purposes of IT-business alignment. The methodology is developed using the principles of formal model checking applied to the enterprise architecture. In this case, the required properties of the enterprise model are expressed by formulas of a certain dialect of formal logic, and the consistency checks are reduced to an exhaustive analysis of the entire space of its states (Clark et. al., 2008). As a verification tool, the language and relational logic of the Alloy Analyzer system (http://alloy.mit.edu/alloy/) (Jackson, 2006) is selected. The tool allows to analyze the model represented in terms of relational logic by automatically generating sample structures, and to check properties of the model by generating counter-examples.
The core of our methodology consists of a new ArchiMate meta-model expressed in terms of MIT AlloyAnalyzer, and a generic algorithm for translation ArchiMate models to corresponding models in terms of relational logic. We also propose 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.