Формальне визначення шаблонів бізнес-процесів представлено на підставі аналізу бібліотек ІTІL і MOF. Визначено передумову ініціалізації і постумову для шаблонів бізнес-процесів. Доведено можливість розв’язання проблеми формальної верифікації для шаблонів бізнес-процесів щодо визначеної передумови ініціалізації і постумови виконання. Планується подальша робота в двох напрямках: застосування запропонованого алгоритму формальної верифікації на інших бібліотеках шаблонів бізнес-процесів та дослідження інших бібліотек бізнес-процесів для їх ідентифікації.
The formal definition of business process templates is presented based on the analysis of ITIL and MOF libraries. The definition of initialization precondition and execution postcondition is introduced. The solvability of formal verification problem for business process templates with respect to the defined initialization precondition and execution postcondition is shown. It is planned to continue this research in two fields: (i) to apply the formal verification algorithm with other business process template libraries and (ii) to examine other business process libraries to identify new classes of business processes.