Printer Friendly

Extended Petri nets for treatment of faults.

1. INTRODUCTION

The correctness and rationality of a workflow model are critical when implementing a successful workflow management, while a workflow containing abnormalities and errors may lead to the failed execution of business processes.

Verifying the workflow plays a very important role in the workflow analysis. The verification of a workflow usually includes three main aspects (Zeng et al., 2007):

Structure verification--Structure verification aims at verifying the structure consistency of a workflow, including deadlock, livelock, lack of synchronization, misuse of modelling objects and constructors, active end, dead activity.

Temporal verification--In reality, activities are executed along the time dimension. Therefore, temporal constraint is an important attribute of workflow specifications. The analysis of temporal constraint is intended to verify the temporal consistency of a workflow specification.

Resource verification--in a workflow, activities need to access resources during their execution. Resource verification aims at verifying whether there are any resource conflicts between different activities in a workflow.

RELATED RESEARCH: The real processes become more and more complex and require adequate models and tools for their improvement. Petri nets and their derivates are a powerful tool that have formal capabilities for analysis and are extensively studied in literature (van Hee et al., 2005; van Hee et al., 2006; Zeng et al., 2008).

2. PRELIMINARIES

Definition 1: A Petri net is a tuple N = <p,T,[F.sup.+],[F.sub.-]>, where:

* P and T are two disjoint non-empty finite sets of places and transitions respectively;

* [F.sup.+] and F are mappings of (P x T) [right arrow] N that are flow functions from transitions to places and fron places to transitions respectively.

F = [F.sup.+] - [F.sup.-] is the incidence matrix of net N.

Definition 2: A Petri net N, is live if, for every reachable state M' and every transitions t there is a state M" reachable from M' which enables t.

Definition 3: A Petri net N, is bounded if, there is a natural number n proving that for every reachable state and every place p the number of tokens in p is less than n.

Formally, the notion of soundness is that for any possible behaviour, there is always a possibility to complete the execution and reach the final state, or to report an exception.

We define an extended net as being [bar.N] = ([bar.P],[bar.T],[bar.F],[bar.W]) , where P = [bar.P], [bar.T] = T [union] {[t.sup.*]}, [bar.F] = F [union] {<f,[t.sup.*]>, <[t.sup.*],i>} and for <x,y> [member of] F,[bar.W] (<x,y>) = W(<x,y>), [bar.W](<f,[t.sup.*]>)=[bar.W](<[t.sup.*],i> = 1).

Transitions [t.sup.*] connects f and i.

Theorem 1: (van der Aalst et al., 2000) A WF net N, is sound if and only if ([bar.N], i) is live and bounded.

Definition 4: (van Hee et al., 2005) A Petri net N is a Workflow net (WF-net) if:

1. N has two special places (or transitions): an initial place i([sup.*]i = [empty set]) and final place f ([f.sup.*] = [empty set]).

2. for any node n [member of] (P [union] T) there exists a path from i to n and from n to f

Traditional WF nets are EWF (Extended Workflow) nets with the empty set of exception transitions.

EWF nets provide a number of advantages from the modelling point of view. First and foremost, they make a clear distinction between normal termination and termination caused by an exception. Unlike traditional WF nets, where special care should be taken to remove all tokens present in the system when an exception situation is encountered, no similar overhead is incurred by EWF nets.

An important correctness property of EWF nets is soundness. Classical WF nets are called sound if one can reach the final marking from any marking reachable from the initial marking (van Hee et al., 2005). The intuition behind this notion is that no matter what happens, there is always a way to complete the execution and reach the final state (proper termination).

Two nets can be combined to produce a new net by means of sequential (*) and parallel ([parallel) composition and choice (+).

Let N be a Petri nets. Then N is a state machine (SM) if

[for all]t [member of] T: [absolute value of [sup.*]t] = 1 [conjunction] [absolute value of [t.sup.*]] = 1.

Definition 5: A WF net N = <[P.sub.p] [union] [P.sub.r], T[F.sup.+.sub.p] [union] [F.sup.+.sub.pr], [F.sup.-.sub.p] [union] [F.sup.-.sub.r] with initial and final places i, f [member of] [P.sub.p] is a RCWF (Resource-Constrained Workflow) net with the set [P.sub.p] of production places and the set [P.sub.r] of resource places, if:

* [P.sub.p] [union] [P.sub.r] = [empty set];

* [F.sup.+.sub.p], [F.sup.-.sub.p] are mappings ([P.sub.p] x T) [right arrow] N;

* [F.sup.-.sub.r], [F.sup.-.sub.r] are mappings ([P.sub.p] x T) [right arrow] N;

* [N.sub.p] = <[P.sub.p], T, [F.sup.+.sub.p], [F.sup.-.sub.r]) is a WF net, which call production net of N.

Definition 6: An RCWF net N is called a state machine workflow net with one resource type (SM1WF) if [P.sub.r] = {r} and the production net [N.sub.p] of N is a state machine.

A necessary and sufficient condition for the soundness of SM1WF-nets will be detailed in the following. We start by introducing the notion of path used here. Unlike a trace, a path does not deal with the processing of multiple production tokens.

Formally, given an SM1WF-net N, a path is a sequence [t.sub.1] ... [t.sub.n] of transitions in T such that [for all]k :1 [less than or equal to] k < n : [t.sup.0.sub.k] = [sup.0][t.sub.k+1]. We write [sup.0][sigma] and [[sigma].sup.0] for the input and the output place of a nonempty path [sigma] = [t.sub.1] ... [t.sub.n], i.e. for [sup.0][t.sub.1], [t.sup.0.sub.n], respectively.

With every path we associate three numbers: resource production, consumption and effect.

The notion of effect allows us to distinguish three kinds of paths. A path [sigma] is called a C-path (consumption path) if [epsilon]([sigma]) < 0, an E-path (equality path) if [epsilon]([sigma]) = 0, and a P-path (production path) if [epsilon]([sigma]) > 0.

Lemma 1: (Interchange Lemma).(van Hee., et al., 2005) Let M, M' be markings and [sigma], [rho] be paths such that [epsilon]([sigma]) [less than or equal to] 0 [less than or equal to] [epsilon]([rho]), and [rho] is not a successor of [sigma]. If [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Theorem 2: (van Hee., et al., 2005) An SM1WF net N is sound if there exists a unique place invariant W such that W(i) = W(f) = 0, W(r) = 1, and moreover W(p) [greater than or equal to] 0 for all p [member of] [P.sub.p], and for each C-path [rho] there is a successor P-path [sigma] such that P([rho]) [greater than or equal to] C([sigma]).

Note that the net may be unsound if it contains a deadlock (a nonterminal marking where there are not enough resources to proceed any further even with one single step) or a livelock (there are always enough resources to make a following step, but all possible steps are not "progress"-steps, i.e. we cannot leave the cycle in order to terminate properly).

A fault is defined as an interruption to the ability of an item to perform a specific function, hence we adopt a mode generic definition, i.e. the term fault is synonymous with failure, errors, mistake, or disturbance that leads to undesirable or intolerable behaviour of equipment.

The fault treatment should be appropriate for each level of the manufacturing system. The fault recovery process can be executed in two ways (Riascos et al., 2004):

* adjusting operational parameters without changing or reorganizing the logical structure of the machine;

* utilization of redundant resources, which can result in low-performance, high cost, weight, and complexity.

3. EXTENDED NET FOR TREATMENT OF FAULTS

We expand the semantics of extended SM1WF nets by introducing, where for any particular fault [d.sub.i] in a specially place from transition [t.sub.i] who generate the fault, lead in location [p.sub.k] a colour token [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Nested Petri nets are Petri nets in which tokens can be Petri nets themselves, called token nets (van Hee et al., 2006).

To the original net we connect a nested net (subnet) for every type of fault. Transition is able to generate a simultaneously number of faults. In this case, the id-token represents [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (see fig. 1.).

Definition 7: (Mateia, 2009) We define an extended net [N.sub.e] as a SM1WF net in which for every fault [d.sub.i], an output place [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is attached to the transition [t.sub.j] which generated the fault; at the moment of the occurrence of the fault generated by the firing of the transition [t.sub.j], a token being coloured [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is attached to the output place.

Theorem 3. (Mateia, 2009) The net [N.sub.e] (from definition 7) is sound.

Soundness of a [N.sub.e] net can be checked by checking that the closure of a [N.sub.e] net is live and bounded. The closure is obtained by adding to [N.sub.e] a transition with f is the input place and i is the output place.

[FIGURE 1 OMITTED]

4. CONCLUSIONS AND FURTHER WORKS

The above model will be analysed and the faults and errors that can appear in the manufacturing process will be detailed. Based on it, the capability of the model to represent, detect and correct the faults and errors will be formalized.

5. REFERENCES

van der Aalst W.M.P. & Hofstede A.H.M. (2000). Verification of Workflow Task structures: A Petri-net-based approach, Information Systems, ISSN:0306-4379, 43-69

Frank P. M. (1992). Principles of Model-based Fault Detection, Proceeding of the International Symposium on AI in Real-time Control, Delpft (363-370)

van Hee, K.; Sidorova, N. & Voorhoeve, M. (2006). Resource-Constrained Workflow Nets Fundamenta InformaticaeXX 2006, ISSN 0169-2968 (243-257) IOS Press

van Hee, K.; Lomazova, I. A.; Oanea O.; Serebrenik, A.; Sidorova, N. & Voorhoeve, M. (2006). Nested nets for adaptive systems, Petri Nets and Other Models of Concurrency-ICAPN2006, ISSN 0302-9743, 241-260

van Hee, K.; Serebrenik, A.; Sidorova, N. & Voorhoeve M. (2005). Soundness of Resource-Constrained Workflow Nets, Aplications and Theory Of Petri Nets, 250-267, ISSN 0302-9743

Mateia, N. A. (2009). Models and algorithm for operative programming production, Phd Thesis

Riascos, L. A. M. & Moscato, L. A. & Miyagi P. E. (2004). Detection and Treatmeant of Faults in Manufacturing Systems Based on Petri Nets, Journal of the Brazilian Society of Mechanical Sciences and Engineering, ISSN 1678-5878

Siegeris, J. & Zimmermann, A. (2006). Workflow Model Compositions Preserving Relaxed Soundness, Lecture Notes in Computer Science, ISSN 0302-9743, 177-192

Zimmermann, A.; Kuhnel, A. & Hommel G. (1998). A Modelling and Analysis Method for Manufacturing Systems Based on Petri Nets, Proc. Computational Engineering in Systems Applications (CESA'98), Nabeul-Hammamet, pages 276-281

Zeng,Q.; Wang,H.; Xu,D.; Duan H. & Han Y. (2007). Conflict detection and resolution for workflows constrained by resources and non-determined durations, The Journal of Systems and Software 81, ISSN 0164-1212 (1491-1504)
COPYRIGHT 2009 DAAAM International Vienna
No portion of this article can be reproduced without the express written permission from the copyright holder.
Copyright 2009 Gale, Cengage Learning. All rights reserved.

Article Details
Printer friendly Cite/link Email Feedback
Author:Mateia, Nicolae Adrian; Rada, Danut; Rada, Doina; Cechin-Crista, Dan
Publication:Annals of DAAAM & Proceedings
Article Type:Report
Geographic Code:4EUAU
Date:Jan 1, 2009
Words:1919
Previous Article:Seamless image-page alignment and rectangular areas removal.
Next Article:Image retrieval queries in description logic.
Topics:

Terms of use | Privacy policy | Copyright © 2019 Farlex, Inc. | Feedback | For webmasters