Метод определения противоречий в demo-моделях бизнес-процессов

В статье рассматривается проблема обнаружения логических противоречий в моделях бизнес процессов и предлагается способ решения этой проблемы с иллюстрацией на примере анализа сложных бизнес-процессов системы здравоохранения на основе формального подхода реляционной логики. Предлагаемый способ должен способствовать повышению эффективности управления муниципальными учреждениями здравоохранения прежде всего в аспекте повышения качества предоставления комплексных услуг для лиц пожилого возраста. Предлагаемый метод основан на формальных инструментах реляционной логики системы моделирования MIT Alloy Analyzer. Для моделирования бизнес-процессов был выбран перспективный подход онтологии организации и конкретная методология моделирования DEMO (Design & Engineering Methodology for Organizations). Эта методология дает возможность полного и объективного описания организации и функционирования современного предприятия. Анализ построенных по методологии DEMO моделей организации позволяет получить детальное представление о процессах управления и взаимодействия и служит основой для проведения бизнес-реинжиниринга и развития информационной инфраструктуры, согласованной с требованиями бизнеса. Важной частью нашего исследования является разработка формальных спецификаций построенных моделей бизнес-процессов, пригодных для применения формальных методов верификации. Поэтому с целью повторного использования разработанных нами методов трансляции моделей бизнес-процессов на язык системы Alloy Analyzer была создана метамодель ключевых конструктивных элементов методологии моделирования DEMO. На основе разработанной мета-модели и конкретных бизнес-процессов предоставления медицинских услуг в ходе исследования были построены формальные модели и проведен анализ их логической непротиворечивости,