{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:48:23Z","timestamp":1781106503138,"version":"3.54.1"},"reference-count":37,"publisher":"IGI Global Scientific Publishing","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,1]]},"abstract":"<jats:p>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. The authors 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 a methodology, they use ArchiMate standard for a conceptual enterprise architecture description language which is fully aligned with TOGAF. The authors also offer several important verification queries and demonstrate practical applicability of their approach using a software prototype of the modeling tool which exploits MIT Alloy Analyzer model checking framework integrated with AchiMate Archi workbench.<\/jats:p>","DOI":"10.4018\/ijismd.2019010101","type":"journal-article","created":{"date-parts":[[2019,3,27]],"date-time":"2019-03-27T14:25:36Z","timestamp":1553696736000},"page":"1-19","source":"Crossref","is-referenced-by-count":0,"title":["A Methodology for Automatic Formal Verification of Enterprise Architecture"],"prefix":"10.4018","volume":"10","author":[{"given":"Eduard","family":"Babkin","sequence":"first","affiliation":[{"name":"National Research University \u201cHigher School of Economics,\u201d Nizhni Novgorod, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pavel","family":"Malyzhenkov","sequence":"additional","affiliation":[{"name":"National Research University \u201cHigher School of Economics,\u201d Nizhni Novgorod, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marina","family":"Ivanova","sequence":"additional","affiliation":[{"name":"National Research University \u201cHigher School of Economics,\u201d Nizhni Novgorod, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikita","family":"Ponomarev","sequence":"additional","affiliation":[{"name":"National Research University \u201cHigher School of Economics,\u201d Nizhni Novgorod, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"IJISMD.2019010101-0","unstructured":"Babkin, E., Buzueva, A., & Logvinova, K. (2014). A method for determination of controversies in DEMO-models of business processes. Business Informatics, 2(28), 33-43."},{"key":"IJISMD.2019010101-1","doi-asserted-by":"publisher","DOI":"10.17323\/1998-0663.2017.3.30.40"},{"key":"IJISMD.2019010101-2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04947-7_8"},{"key":"IJISMD.2019010101-3","doi-asserted-by":"publisher","DOI":"10.1111\/j.1365-2575.2011.00379.x"},{"key":"IJISMD.2019010101-4","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-009-0120-5"},{"issue":"1","key":"IJISMD.2019010101-5","first-page":"43","article-title":"Comparing strategic IT alignment versus process IT alignment in SMEs.","volume":"44","author":"A.Cataldo","year":"2012","journal-title":"Journal of Research and Practice in Information Technology"},{"key":"IJISMD.2019010101-6","doi-asserted-by":"publisher","DOI":"10.1109\/TEM.2005.861804"},{"key":"IJISMD.2019010101-7","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.10.002"},{"key":"IJISMD.2019010101-8","author":"T.Clark","year":"2008","journal-title":"Applied meta-modeling: A foundation for language driven development"},{"key":"IJISMD.2019010101-9","first-page":"1","article-title":"Strategic IT alignment: Twenty-five years on.","author":"T.Coltman","year":"2015","journal-title":"Journal of Information Technology"},{"key":"IJISMD.2019010101-10","author":"J. S.Fitzgerald","year":"2008","journal-title":"Vienna development method. In Wiley encyclopedia of computer science and engineering"},{"key":"IJISMD.2019010101-11","doi-asserted-by":"publisher","DOI":"10.4018\/ijismd.2015010101"},{"key":"IJISMD.2019010101-12","doi-asserted-by":"publisher","DOI":"10.25300\/MISQ\/2014\/38.4.10"},{"issue":"3","key":"IJISMD.2019010101-13","first-page":"1","article-title":"Six Types of IT-Business Strategic Alignment: An investigation of the constructs and their measurement","volume":"24","author":"J. E.Gerow","year":"2014","journal-title":"European Journal of Information Systems"},{"issue":"1","key":"IJISMD.2019010101-14","first-page":"4","article-title":"Strategic alignment: Leveraging information technology for transforming organizations","volume":"38","author":"J. C.Henderson","year":"1993","journal-title":"IBM Systems Journal"},{"key":"IJISMD.2019010101-15","author":"D.Jackson","year":"2006","journal-title":"Software abstractions: Logic, language and analysis"},{"key":"IJISMD.2019010101-16","unstructured":"Jonkers, H., Band, I., & Quartel, D. (2012). The ArchiSurance case study [White paper]. The Open Group."},{"key":"IJISMD.2019010101-17","author":"Y. G.Karpov","year":"2009","journal-title":"Model checking. Verifikatsiya parallel\u2019nykh i raspredelennykh programmnykh sistem"},{"key":"IJISMD.2019010101-18","doi-asserted-by":"publisher","DOI":"10.1016\/S0963-8687(00)00049-4"},{"key":"IJISMD.2019010101-19","author":"K.Lano","year":"2012","journal-title":"The B language and method: A guide to practical formal development"},{"key":"IJISMD.2019010101-20","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/978-3-642-38613-8_4","article-title":"Translating VDM to alloy.","author":"K.Lausdahl","year":"2013","journal-title":"International Conference on Integrated Formal Methods"},{"key":"IJISMD.2019010101-21","doi-asserted-by":"publisher","DOI":"10.1201\/1078\/43647.20.4.20030901\/77287.2"},{"key":"IJISMD.2019010101-22","doi-asserted-by":"publisher","DOI":"10.2307\/41166021"},{"key":"IJISMD.2019010101-23","doi-asserted-by":"publisher","DOI":"10.17323\/1998-0663.2017.3.56.64"},{"key":"IJISMD.2019010101-24","unstructured":"Malyzhenkov, P., & Ivanova, M. (2018). The Intellectual Dimension of IT-Business Alignment Problem: Alloy Application. In Enterprise and Organizational Modeling and Simulation, 14th International Workshop, EOMAS 2018, Tallinn, Estonia, June 11\u201312. Springer."},{"key":"IJISMD.2019010101-25","unstructured":"Queiroz, M., & Coltman, T. (2014). Reorienting the information systems function to support increasing levels of business service. In International Conference on Information Systems(ICIS), Auckland, New Zealand."},{"issue":"1","key":"IJISMD.2019010101-26","article-title":"Aligning Business and IT Strategies in Multi-Business Organizations","volume":"30","author":"P.Reynolds","year":"2015","journal-title":"Journal of Information Technology"},{"key":"IJISMD.2019010101-27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24369-6_11"},{"key":"IJISMD.2019010101-28","doi-asserted-by":"publisher","DOI":"10.2307\/23044052"},{"key":"IJISMD.2019010101-29","unstructured":"The Global IT Trends Survey. (2017). Retrieved from http:\/\/www.globaliim.com\/"},{"key":"IJISMD.2019010101-30","unstructured":"The Open Group. (2013). Archimate 2.1 Specification. Open Group Standard. Zaltbommel: Van Haren Publishing. Retrieved from https:\/\/www.vanharen.net\/Samplefiles\/9789401800037SMPL.pdf"},{"key":"IJISMD.2019010101-31","unstructured":"The Open Group. (n.d.). Architecture Framework (TOGAF Version 9.1). Retrieved from http:\/www.opengroup.org\/"},{"key":"IJISMD.2019010101-32","volume":"Vol. 295","author":"B.Ulitin","year":"2017","journal-title":"Ontology and DSL co-evolution using graph transformations methods, Lecture Notes in Business Information Processing"},{"key":"IJISMD.2019010101-33","doi-asserted-by":"publisher","DOI":"10.1016\/0263-2373(93)90037-I"},{"issue":"10","key":"IJISMD.2019010101-34","article-title":"The Impact of Strategic IT-Business Alignment: Evidence from Saudi Private Small and Midsize Enterprises","volume":"8","author":"A.Waleed","year":"2017","journal-title":"International Journal of Business and Social Science"},{"key":"IJISMD.2019010101-35","doi-asserted-by":"publisher","DOI":"10.1109\/SOLI.2008.4686496"},{"key":"IJISMD.2019010101-36","unstructured":"Warmer, J.B., & Kleppe, A.G. (1998). The object constraint language: Precise modeling with UML."}],"container-title":["International Journal of Information System Modeling and Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=226233","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T16:19:51Z","timestamp":1651767591000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJISMD.2019010101"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2019,1]]},"references-count":37,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.4018\/ijismd.2019010101","relation":{},"ISSN":["1947-8186","1947-8194"],"issn-type":[{"value":"1947-8186","type":"print"},{"value":"1947-8194","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1]]}}}