Скрыть
Раскрыть

ISSN 1998-0663 (print),
ISSN 2587-8166 (online)

English version: ISSN 2587-814X (print),
ISSN 2587-8158 (online)

Бабкин Э. А. 1, Пономарев Н. О. 
  • 1 НИУ ВШЭ, 603014, Россия, Нижний Новгород, Сормовское шоссе, д.30

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

2017. № 3 (41). С. 30–40 [содержание номера]

Э.А. Бабкин - кандидат технических наук, PhD in Computer Science, профессор кафедры информационных систем и технологий, Национальный исследовательский университет «Высшая школа экономики»
Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20
E-mail: eababkin@hse.ru

Н.О. Пономарев - студент магистерской программы «Бизнес-информатика», Национальный исследовательский университет «Высшая школа экономики»; инженер группы разработки программного обеспечения АО «Интел»
Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20
E-mail:nik4nikita@gmail.com

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

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

Библиографическое описание: Бабкин Э.А., Пономарев Н.О. Анализ непротиворечивости моделей архитектуры предприятия с использованием формальных методов верификации // Бизнес-информатика. 2017. № 3 (41). С. 30–40.  DOI: 10.17323/1998-0663.2017.3.30.40. 
BiBTeX
RIS
 
 
Rambler's Top100 rss