@ARTICLE{26583204_212183168_2017, 
	author = {Э. А. Бабкин and Н. О. Пономарев}, 
	keywords = {, архитектура предприятия, ArchiMate, Alloy Analyzer, верификация, анализ непротиворечивостиформальные методы},
	title = {Анализ непротиворечивости моделей архитектуры предприятия с использованием формальных методов верификации},
	journal = {Бизнес-информатика},
	year = {2017},
	number = {3 (41)},
	pages = {30-40},
	url = {https://bijournal.hse.ru/2017--3 (41)/212183168.html},
	publisher = {},
	abstract = {Э.А. Бабкин - кандидат технических наук, PhD in Computer Science, профессор кафедры информационных систем и технологий, Национальный исследовательский университет «Высшая школа экономики»Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20E-mail: eababkin@hse.ruН.О. Пономарев - студент магистерской программы «Бизнес-информатика», Национальный исследовательский университет «Высшая школа экономики»; инженер группы разработки программного обеспечения АО «Интел»Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20E-mail:nik4nikita@gmail.com      Разработка архитектуры предприятия является сложным процессом, но в то же время позволяет решить проблему синхронизации возможностей и потребностей бизнеса и информационных технологий (ИТ). Решение данной проблемы достигается за счет уточнения понимания и формализации описания бизнес-процессов и взаимодействия элементов системы путем их формального описания. Наличие большого числа взаимодействующих бизнес-процессов и сущностей архитектуры предприятия объясняет необходимость проверки их корректности. Поэтому необходимо их автоматически верифицировать, на основе формализации требований к архитектуре.      В данной работе предлагается метод обнаружения логических противоречий в моделях архитектуры предприятия, на основе частного случая подхода к проверке моделей, примененного в бизнес-моделировании. В качестве языка описания архитектуры предприятия в работе используется современный открытый и независимый язык ArchiMate. Разрабатываемый The Open Group стандарт предоставляет общую спецификацию для описания построения и функционирования бизнес-процессов, организационных структур, информационных потоков, ИТ-систем и технической инфраструктуры предприятия. В качестве верификатора выбран формальный язык реляционной логики и инструментарий системы MITAlloy Analyzer, позволяющий выполнять анализ ограничений модели в терминах реляционной логики путем автоматической генерации структур, которые удовлетворяют требованиям логической модели.      В данной работе предлагается упростить и автоматизировать процесс спецификации и верификации моделей предметной области архитектуры предприятия с помощью визуального редактора конструирования моделей на языке ArchiMate - Archi. Разработанный авторами плагин к редактору осуществляет трансляцию моделей архитектуры предприятия на язык системы Alloy Analyzer и в качестве основы для построения конкретных моделей предметной области использует метамодель ключевых элементов спецификации ArchiMate. Предложенный метод и программные решения апробированы на примере пользовательского кейса архитектуры предприятия компании ArciSurance.Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 16-06-00184 А «Разработка и исследование моделей online-дискуссии на материале обсуждения политических новостей»},
	annote = {Э.А. Бабкин - кандидат технических наук, PhD in Computer Science, профессор кафедры информационных систем и технологий, Национальный исследовательский университет «Высшая школа экономики»Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20E-mail: eababkin@hse.ruН.О. Пономарев - студент магистерской программы «Бизнес-информатика», Национальный исследовательский университет «Высшая школа экономики»; инженер группы разработки программного обеспечения АО «Интел»Адрес: 603155, г. Нижний Новгород, ул. Большая Печерская, д. 25/20E-mail:nik4nikita@gmail.com      Разработка архитектуры предприятия является сложным процессом, но в то же время позволяет решить проблему синхронизации возможностей и потребностей бизнеса и информационных технологий (ИТ). Решение данной проблемы достигается за счет уточнения понимания и формализации описания бизнес-процессов и взаимодействия элементов системы путем их формального описания. Наличие большого числа взаимодействующих бизнес-процессов и сущностей архитектуры предприятия объясняет необходимость проверки их корректности. Поэтому необходимо их автоматически верифицировать, на основе формализации требований к архитектуре.      В данной работе предлагается метод обнаружения логических противоречий в моделях архитектуры предприятия, на основе частного случая подхода к проверке моделей, примененного в бизнес-моделировании. В качестве языка описания архитектуры предприятия в работе используется современный открытый и независимый язык ArchiMate. Разрабатываемый The Open Group стандарт предоставляет общую спецификацию для описания построения и функционирования бизнес-процессов, организационных структур, информационных потоков, ИТ-систем и технической инфраструктуры предприятия. В качестве верификатора выбран формальный язык реляционной логики и инструментарий системы MITAlloy Analyzer, позволяющий выполнять анализ ограничений модели в терминах реляционной логики путем автоматической генерации структур, которые удовлетворяют требованиям логической модели.      В данной работе предлагается упростить и автоматизировать процесс спецификации и верификации моделей предметной области архитектуры предприятия с помощью визуального редактора конструирования моделей на языке ArchiMate - Archi. Разработанный авторами плагин к редактору осуществляет трансляцию моделей архитектуры предприятия на язык системы Alloy Analyzer и в качестве основы для построения конкретных моделей предметной области использует метамодель ключевых элементов спецификации ArchiMate. Предложенный метод и программные решения апробированы на примере пользовательского кейса архитектуры предприятия компании ArciSurance.Исследование выполнено при финансовой поддержке РФФИ в рамках научного проекта № 16-06-00184 А «Разработка и исследование моделей online-дискуссии на материале обсуждения политических новостей»}
}