Целью выпускной работы является повышение качества моделей BPMN 2.0 за счет создания средства проверки моделей с применением алгоритма Model Checking, который поддерживается в верификаторе SPIN, с использованием языка Promela. Произведён обзор существующих методов верификации моделей, дана сравнительная характеристика рассмотренных работ. По результатам сравнительного анализа представлен подход к верификации бизнес-процессов и предложена архитектура для реализации метода в программном средстве. В работе описаны детали реализации программного обеспечения и методы оценки качества разработанного программного обеспечения. Эффективность разработанного средства была оценена в ходе проведения нескольких экспериментов, в ходе одного из которых была выявлена ошибка в одном из рассмотренных бизнес-процессов.

The aim of the graduation project is to improve the quality of Business Process Modeling Notation (BPMN) 2.0 models by creating a tool for verifying them using the Model Checking algorithm supported by the SPIN verifier and the Promela language. To achieve this goal, a review of existing methods for model verification is considered and comparative analysis of the works is provided. Based on the results of this analysis, an approach to business process verification and propose an architecture for implementing it in a software tool are considered. The paper describes in detail the software implementation process and methods for assessing the quality of the developed software. The effectiveness of the tool is evaluated through several experiments, during which an error in one of the considered business processes was identified.