Анализ непротиворечивости моделей архитектуры предприятия с использованием формальных методов верификации

Бизнес-информатика. 2017. Т. 43. № 3. С. 30–40.

Бабкин Э. А., Пономарев Н. О.

Разработка архитектуры предприятия является сложным процессом, но в то же время позволяет решить проблему синхронизации возможностей и потребностей бизнеса и информационных технологий (ИТ). Решение данной проблемы достигается за счет уточнения понимания и формализации описания бизнес-процессов и взаимодействия элементов системы путем их формального описания. Наличие большого числа взаимодействующих бизнес-процессов и сущностей архитектуры предприятия объясняет необходимость проверки их корректности. Поэтому необходимо их автоматически верифицировать, на основе формализации требований к архитектуре.
      В данной работе предлагается метод обнаружения логических противоречий в моделях архитектуры предприятия, на основе частного случая подхода к проверке моделей, примененного в бизнес-моделировании. В качестве языка описания архитектуры предприятия в работе используется современный открытый и независимый язык ArchiMate. Разрабатываемый The Open Group стандарт предоставляет общую спецификацию для описания построения и функционирования бизнес-процессов, организационных структур, информационных потоков, ИТ-систем и технической инфраструктуры предприятия. В качестве верификатора выбран формальный язык реляционной логики и инструментарий системы MITAlloy Analyzer, позволяющий выполнять анализ ограничений модели в терминах реляционной логики путем автоматической генерации структур, которые удовлетворяют требованиям логической модели.
      В данной работе предлагается упростить и автоматизировать процесс спецификации и верификации моделей предметной области архитектуры предприятия с помощью визуального редактора конструирования моделей на языке ArchiMate – Archi. Разработанный авторами плагин к редактору осуществляет трансляцию моделей архитектуры предприятия на язык системы Alloy Analyzer и в качестве основы для построения конкретных моделей предметной области использует метамодель ключевых элементов спецификации ArchiMate. Предложенный метод и программные решения апробированы на примере пользовательского кейса архитектуры предприятия компании ArciSurance.

Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 16-06-00184 А «Разработка и исследование моделей online-дискуссии на материале обсуждения политических новостей»

Ключевые слова: formal methods, формальные методы, архитектура предприятия, enterprise architecture, ArchiMate, consistency analysis, ArchiMate, анализ непротиворечивости