Algorithm for formal verification of business process templates
- PDF / 174,035 Bytes
- 13 Pages / 595.276 x 793.701 pts Page_size
- 16 Downloads / 190 Views
ALGORITHM FOR FORMAL VERIFICATION OF BUSINESS PROCESS TEMPLATES UDC 519.681
A. S. Varosyan
Abstract. 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. Keywords: business process, template, formal verification.
In the present article, the problem of formally checking business process templates (BPTs) for correctness is considered. Since the problem of formal verification of business processes is unsolvable in the general case, the need arises for the construction of formally verified subclasses of business processes that are of practical interest. As is well known, 70% of the cost of management of business processes is spent on the service of existing processes and only 30% is spent on the development of new business processes [1]. It is also well known that more than $300 million per year are spent on the redesign of existing processes [1, 2]. This leads to the necessity of creation of libraries of business process templates or libraries of parametrized process descriptions that will allow one to obtain concrete processes by specifying their parameter values [3]. In this work, a formally verified subclass of business process templates is defined that, as is shown below, contains all templates of some widely used template libraries [3, 4]. The subclass of templates being considered is determined by the specification of base elements and operations over them with the help of which users can construct an arbitrary template of the subclass. The problem of formal verification of templates is shown to be reducible to the problem of formal verification of base elements. Algorithms of polynomial complexity are constructed for the verification of template elements, and, based on these algorithms, a general verification algorithm is constructed that also has polynomial complexity. The model described in the IBM MQSeries Workflow [7] is chosen as the basic model. This model is extended with the help of constructions necessary for the consideration of the formal verification problem that presumes the specification of pre- and postconditions of a process, i.e., initiation and termination conditions of the process. A process is called (partially) correct if, whenever its precondition is satisfied and it is successfully completed, its postcondition is satisfied. A process is called (completely) correct if, whenever its precondition is satisfied, it terminates and its postcondition is satisfied. This article considers the problem of partial correctness (correctness i
Data Loading...
