Algorithm for formal verification of business process templates

A formal definition of a business process template is presented that is based on an analysis of ITIL and MOF libraries. Definitions of an initialization precondition and an execution postcondition are introduced. The solvability of the formal verification problem for business process templates is shown under some given initialization precondition and execution postcondition. This research is planned to be continued with a view to (i) using a formal verification algorithm with other business process template libraries and (ii) examining other business process libraries to identify new classes of business processes.