A Petri-net approach to refining object behavioural specifications.

1 Introduction

In the past two decades, object orientation has been an influential discipline in software engineering (1). According to the principles of object orientation, an object is an entity that encapsulates states and behaviours. A system is considered as a collection of objects which are interacting with others in order to accomplish the system functionalities. It can be abstracted in two aspects (structure and behaviour) and two levels (intra-object and inter-object) as shown in Figure 1 [1, 2, 3, 4, 5, 6, 7, 8, 9]. Structurally, objects with the same attributes are grouped into classes while classes having common attributes are generalised to form an inheritance hierarchy. Objects exhibit different behaviours on interacting with others, thus demonstrating different object interaction scenarios. This paper investigates the behavioural aspect of objects.

In object-oriented system design, the functional requirements of a system are given by the end-users as use cases--the typical cases of how a system can be used [10, 11]. These use cases are elaborated and expressed in terms of object interaction scenarios and specified as UML sequence diagrams and collaboration diagrams [11, 12, 13, 14, 15, 16]. We need to create, from the object interaction scenarios, object-based specifications In this refinement process, at least the following problems have to be tackled.

[FIGURE 1 OMITTED]

Specification constructs for object interaction scenarios being too primitive. Conventional specification constructs for object interaction scenarios lacks the formality for representing the pre-conditions and post-conditions for each event occurrence. These are however essentially required in deriving the object behavioural specifications, where the conditions, events and their causal relationships need to be explicitly specified.

Different abstractions between intra-object lifecycle and inter-object interaction. It is difficult to derive individual object behaviours (within a single object lifecycle) from the object interaction scenarios (among multiple objects) because of the difference in abstraction (intra-object versus inter-object). In the literature of object-oriented system design, there is a lack of systematic approaches to solving this problem satisfactorily.

Difficulty in verifying the correctness of the object behavioural specifications. The object behavioural specifications so derived should be correct in the sense that they reflect exactly the given object interaction scenarios [4, 17, 18, 19, 20]. Without a formal method, one needs to go through all possible object interaction scenarios to ensure correctness of the specifications. The process is time-consuming.

Lack of rigorous methods for analysing the system properties. One major objective in system design is to obtain a live, bounded and reversible system--liveness implies freeness of deadlocks, and boundedness implies absence of capacity overflows, while reversibility refers to recoverability. Without a rigorous analysis method, it is difficult for one to analyse whether the outcome system design is live, bounded and reversible.

In the literature, there are only a few approaches or methods for deriving an object-based behavioural specifications from a given set of use cases or object interaction scenarios. Bordeleau proposed an approach which takes a traceable progression from use cases to the object-based state machines [21, 22]. Dano proposed an approach where the use cases are synthesised into a system design according to some mapping rules [23, 24]. However, these approaches solve only trivial issues. The system design cannot be rigorously analysed on its liveness, boundedness and reversibility. Moreover, they are themselves incomplete and insufficient in the sense that the derived object-based state machines may not reflect exactly the given use cases or object interaction scenarios.

On the other hand, there are approaches or methods which derive a system from a given set of event traces or sequences. Graubmann proposed a method for constructing an elementary net system from a set of event traces [25]. The method is based on the dependence relation between events. A set of possible states and state transitions, which are compatible to the dependence relation, are deduced. Smith proposed a method for constructing a condition-event system from a set of occurrence nets based on the concept of quotient nets [26]. Hiraishi proposed a method for constructing a Petri net from a set of firing sequences [27]. In Hiraishi's method, a language is first identified from the firing sequences. Based on the dependency relation extracted from the language, a safe Petri net is created. Lee also proposed an approach for integration of use cases using constraint-based modular Petri nets [28]. However, without concepts of object-orientation, these approaches and methods cannot be applied to object-oriented system design.

In this paper, based on Petri nets, we propose a method for refining a given set of object interaction scenarios into object-based behavioural specifications, where the above-mentioned problems can be resolved effectively. It involves the following steps :

Step 1. Each object interaction scenario is specified as a labelled Petri net (labelled net) with an AMG-structure (i.e. structurally an augmented marked graph).

Step 2. The labelled nets are synthesised into an integrated net which serves to represent the system. Based on the properties of AMG-structure, the system is analysed.

Step 3. Duplicate labels are eliminated from the integrated net, while preserving the firing sequences (event sequences).

Step 4. Individual object-based specifications are obtained as projections of the integrated net onto the objects.

[FIGURE 2 OMITTED]

Our proposed method offers a number of distinctive features.

Formal specification of object interaction scenarios. The object interaction scenarios are specified as unambiguous and semantically rich labelled nets. The partial orderings of events as well as the causal relationships between events and conditions are explicitly represented.

Effective analysis on the essential system properties. The integrated system possesses an AMG-structure. By making use of the special properties of AMG-structure, the system can be effectively analysed on its liveness, boundedness, reversibility and conservativeness.

Correctness of the derived specifications. Individual object behavioural specifications are rigorously derived from the object interaction scenarios through synthesis and projection. The specifications so obtained reflect exactly the given object interaction scenarios.

Readiness for implementation purposes. In the specifications, every condition or event is uniquely represented so that they can be readily used for implementation purposes.

The rest of this paper is organised as follows. Section 2 provides the preliminaries to be used in this paper. Section 3 introduces the AMG-structure, where augmented marked graphs and their properties are described. In Section 4, we show the formal specification of object interaction scenarios as labelled nets (Step 1 of the proposed method). In Section 5, we focus on synthesising the labelled nets into an integrated system, and analysing the system properties (Step 2 of the proposed method). Section 6 then presents an algorithm for eliminating duplicate labels from the integrated net (Step 3 of the proposed method). In Section 7, we show how individual object-based behavioural specifications are obtained as projections of the integrated net (Step 4 of the proposed method). Section 8 gives a real-life example for illustration. Section 9 concludes this paper.

It should be noted that this paper primarily focus on refinement of object-based behavioural specifications deriving individual object-based specifications from the object interaction scenarios. The structural aspect of an object-oriented system will not be investigated.

2 Preliminaries

This section provides the preliminaries for readers who are not familiar with Petri nets [29, 30, 31, 32].

A place-transition net (PT-net) is a directed graph consisting of two sorts of nodes called places and transitions, such that no arcs connect two nodes of the same sort. Graphically, a place is denoted by a circle, a transition by a box, and an arc by a directed line. A Petri net is a PT-net with some tokens assigned to its places, and the token distribution over its places is denoted by a marking function.

Definition 2.1. A place-transition net (PT-net) is a 4-tuple N = <P, T, F, W>, where P is a set of places, T is a set of transitions, F [subset or equal to] (P x T) [union] (T x P) is a flow relation and W : F [right arrow] { 1, 2,... } is a weight function. N is said to be ordinary if and only if the range of W is { 1 }. An ordinary PT-net is usually written as ( P, T, F ).

Definition 2.2. Let N = ( P, T, F, W > be a PT-net. For x [member of] (P [union] T), *x = {y | (y, x) [member of] F} and x* = { y | (x, y) [member of] F } are called the pre-set and post-set of x, respectively. For X = { [x.sub.1], [x.sub.2], ..., [x.sub.n] } [subset or equal to] (P [union] T), *X = *[x.sub.1] [union] *[x.sub.2] [union] ... [union] *[x.sub.n] and X* = [x.sub.1*] [union] [x.sub.2]* [union] ... [union] [x.sub.n]* are called the pre-set and post-set of X, respectively.

Definition 2.3. For a PT-net N = < P, T, F, W >, a path is a sequence of nodes < [x.sub.1], [x.sub.2], ..., [x.sub.n] >, where ([x.sub.i], [x.sub.i+1]) [member of] F for i = 1, 2, ..., n-1. A path is said to be elementary if and only if it does not contain the same node more than once.

Definition 2.4. For a PT-net N = < P, T, F, W >, a cycle is a sequence of places < [p.sub.1], [p.sub.2], ..., [p.sub,n] > such that [there exists] [t.sub.1], [t.sub.2], ..., [t.sub.n] [member of] T : < [p.sub.1], [t.sub.1], [p.sub.2], [t.sub.2], ..., [p.sub.n], [t.sub.n]) forms an elementary path and ([t.sub.n], [p.sub.1]) [member of] F.

Definition 2.5. For a PT-net N = < P, T, F, W >, a marking is a function M : P [right arrow] { 0, 1, 2, ... } where M(p) is the number of tokens in p. (N, [M.sub.0]) represents N with an initial marking [M.sub.0].

Definition 2.6. For a PT-net N = < P, T, F, W ), a transition t is said to be enabled at a marking M if and only if [for all] p [member of] *t : M(p) [greater than or equal to] W(p,t). On firing t, M is changed to M' such that [for all] p [member of] P : M'(p) = M(p) - W(p,t) + W(t,p). In notation, M [N,t> M' or M [t> M'.

Definition 2.7. For a PT-net (N, [M.sub.0]), a sequence of transitions [sigma] = ([t.sub.1], [t.sub.2], ..., [t.sub.n]) is called a firing sequence if and only if [M.sub.0] [[t.sub.1])... [[t.sub.n]) [M.sub.n]. In notation, [M.sub.0] [N,[sigma]) [M.sub.n] or [M.sub.0] [[sigma]> Mn.

Definition 2.8. For a PT-net (N, [M.sub.0]), a marking M is said to be reachable if and only if there exists a firing sequence [sigma] such that [M.sub.0] [[sigma]) M. In notation, [M.sub.0] [N,*> M or [M.sub.0] [*) M. [N, [M.sub.0]) or [[M.sub.0]> represents the set of all reachable markings of (N, [M.sub.0]).

Definition 2.9. Let N = < P, T, F, W > be a PT-net, where P = { [p.sub.1], [p.sub.2], ..., [p.sub.m]} and T = {[t.sub.1], [t.sub.2], ..., [t.sub.n] }. The incidence matrix of N is an m x n matrix V whose typical entry [v.sub.ij] = W([p.sub.i],[t.sub.j]) - W([t.sub.j],[p.sub.i]) represents the change in number of tokens in [p.sub.i] after firing [t.sub.j] once, for i = 1,2, ..., m and j = 1, 2,..., n.

Liveness, boundedness, safeness, reversibility and conservativeness are well known properties of Petri nets. Liveness implies deadlock freeness. Boundedness refers to the property that the system is free from any potential capacity overflow. Safeness and conservativeness are two special cases of boundedness. Reversibility refers to the capability of a system of being recovered or reinitialised from any reachable state. In general, liveness, boundedness and reversibility collectively characterise a robust or well-behaved system.

Definition 2.10. For a PT-net (N, [M.sub.0]), a transition t is said to be live if and only if [for all] M [member of] [[M.sub.0]>, [there exists] M' : M [*> M' ft). (N, [M.sub.0]) is said to be live if and only if every transition is live.

Definition 2.11. For a PT-net (N, M()), a place p is said to be k-bounded (or bounded) if and only if [for all] M [member of] [[M.sub.0]> : M(p) [less than or equal to] k, where k > 0. (N, [M.sub.0]) is said to be k-bounded (or bounded) if and only if every place is k-bounded.

Definition 2.12. A PT-net (N, [M.sub.0]) is said to be safe if and only if every place is 1-bounded.

Definition 2.13. A PT-net (N, [M.sub.0]) is said to be reversible if and only if [for all] M [member of] [[M.sub.0]): M [*) [M.sub.0].

Definition 2.14. A PT-net (N, [M.sub.0]) is said to be well-behaved if and only if it is live, bounded and reversible.

Definition 2.15. A PT-net N = < P, T, F, W > is said to be conservative if and only if there exists a m-vector a > 0 such that [alpha]V = 0, where m = | P | and V is the incidence matrix of N.

[FIGURE 3 OMITTED]

3 AMG-structure and its properties

AMG-structure refers to an augmented-marked-graph structure. In the literature, augmented marked graphs are not well known, as compared to other sub-classes of Petri nets such as free-choice nets [33]. However, they possess many special properties pertaining to liveness, boundedness and reversibility. This section introduces augmented marked graphs and their special properties.

[FIGURE 4 OMITTED]

Definition 3.1 [34]. An augmented marked graph (N, Mo; R) is an ordinary PT-net (N, [M.sub.0]) with a specific subset of places R, satisfying that : (a) Every place in R is marked by [M.sub.0]. (b) The net (N', [M.sub.0]') obtained from (N, [M.sub.0]; R) by removing the places in R and their associated arcs is a marked graph, (c) For each place r e R, there exist [k.sub.r] [greater than or equal to] 1 pairs of transitions [D.sub.r] = {<[t.sub.s1]), [t.sub.h1]), <[t.sub.s2], [t.sub.h2]),..., <[t.sub.skr], [t.sub.hkr]) }- such that r* = {[t.sub.s1], [t.sub.s2], .... [t.sub.skr]} [subset or equal to] T and *r = {[t.sub.h1], [t.sub.h2], ..., [t.sub.hkr]) [subset or equal to] T and that, for each ([t.sub.si], [t.sub.hi]) [member of] [D.sub.r], there exists in N' an elementary path [[rho].sub.ri] connecting [t.sub.si] to [t.sub.hi]. (d) In (N', [M.sub.0]'), every cycle is marked and no [[rho].sub.ri] is marked.

Figure 4 shows an augmented marked graph (N, [M.sub.0]; R), where R = {[r.sub.1], [r.sub.2]}.

Definition 3.2. Let (N, M") be a PT-net, where R = { [r.sub.1], [r.sub.2], ..., [r.sub.k]} is the set of marked places such that |*[r.sub.i]| > 0 and | [r.sub.i]* | > 0 for i = 1, 2,..., k. (N, [M.sub.0]) is said to be of an AMG-structure if and only if (N, [M.sub.0]; R) is an augmented marked graph.

Definition 3.3. For a PT-net (N, [M.sub.0]), a set of places S is called a siphon if and only if *S [subset or equal to] S*. S is said to be minimal if and only if there does not exist any siphon S' in N such that S' [subset] S. S is said to be empty at a marking M e [[M.sub.0]) if and only if S contains no places which are marked by M.

Definition 3.4. For a PT-net (N, [M.sub.0]), a set of places Q is called a trap if and only if Q* [subset or equal to] *Q. Q is said to be maximal if and only if there does not exist any trap Q' in N such that Q [subset] Q'. Q is said to be marked at a marking M [member of] [[M.sub.0]) if and only if Q contains at least one place which is marked by M.

Property 3.1 [34]. An augmented marked graph is live and reversible if and only if it does not contain any potential deadlock. (Note : A potential deadlock is a siphon which would eventually become empty.)

Definition 3.5. For an augmented marked graph (N, [M.sub.0]; R), a minimal siphon is called an R-siphon if and only if it contains at least one place in R.

Property 3.2 [35, 36]. An augmented marked graph (N, [M.sub.0]; R) is live and reversible if and only if no R-siphons eventually become empty.

Property 3.3 [34, 35, 36]. An augmented marked graph (N, M(); R) is live and reversible if every R-siphon contains a marked trap.

For the augmented marked graph (N, [M.sub.0]; R) shown in Figure 4, each R-siphon contains a marked trap. (N, [M.sub.0]; R) is live and reversible.

Definition 3.6 [37]. Suppose an augmented marked graph (N, [M.sub.0]; R) is transformed into a PT-net (N', [M.sub.0]') as follows. For each r [member of] R, where Dr = {([t.sub.s1], [t.sub.h1]), ([t.sub.s2], [t.sub.h2]), ..., ([t.sub.skr] - [t.sub.hkr]) h replace r with a set of places { [q.sub.1], [q.sub.2], ..., [q.sub.kr]}, such that [M.sub.0]'[[q.sub.i]] = [M.sub.0][r] and [q.sub.i]* = { [t.sub.si] } and *[q.sub.i] = { thi } for i = 1, 2, ..., k,. (N', [M.sub.0]') is called the R-transform of(N, [M.sub.0];R).

Property 3.4 [37]. Let (N\ [M.sub.0]') be the R-transform of an augmented marked graph (N, [M.sub.0]; R). (N, [M.sub.0]; R) is bounded and conservative if and only if every place in (N', [M.sub.0]') belongs to a cycle.

Figure 5 shows the R-transform (N', [M.sub.0]') of the augmented marked graph (N, [M.sub.0]; R) in Figure 4. (N', [M.sub.0]') is bounded, where every place belongs to a cycle. (N, [M.sub.0]; R) is bounded and conservative.

[FIGURE 5 OMITTED]

4 Specifying object interaction scenarios as labelled nets

In this section, we show how an object interaction scenario can be formally specified as a labelled net with an AMG-structure (Step 1 of our proposed method).

A labelled net is a Petri net, where labels are assigned to places and transitions. Usually, places are labelled by conditions to denote specific system substates where the conditions hold, and transitions by events to denote specific occurrences of the events.

Definition 4.1. A labelled Petri net (or labelled net) is a 7-tuple N = < P, T, F, C, E, Lp, Lt), where ( P, T, F) is an ordinary PT-net, C is a set of condition labels, E is a set of event labels, Lp : P [right arrow] C is a function for assigning a condition label to every place, and Lt : T [right arrow] E is a function for assigning an event label to every transition.

Definition 4.2. Let N = < P, T, F, C, E, Lp, Lt) be a labelled net. A place p is said to be uniquely labelled in N if and only if [for all] p' [member of] P : (Lp(p') = Lp(p)) [??] (p' = p). A transition t is said to be uniquely labelled in N if and only if [for all] t' [member of] T : (Lt(t') [??] Lt(t)) => (f = t). N is said to be uniquely labelled if and only if all places and transitions are uniquely labelled.

Figure 6 shows a typical labelled net. Places [p.sub.3], [p.sub.4], [p.sub.5], [p.sub.6], [p.sub.9] and [p.sub.10] are uniquely labelled, whereas [p.sub,1], [p.sub.2], [p.sub.7] and [p.sub.8] are not, as for example, condition label c, appears in [p.sub.1] and [p.sub.7], and [c.sub.2] in [p.sub.2] and [p.sub.8]. Transitions [t.sub.3], [t.sub.4] and [t.sub.5] are uniquely labelled, whereas [t.sub.1], [t.sub.2], [t.sub.6], and [t.sub.7] are not, as for example, event label [e.sub.1] appears in [t.sub.1] and [t.sub.6], and [e.sub.2] in [t.sub.2] and [t.sub.7]. Therefore, the labelled net is not uniquely labelled.

[FIGURE 6 OMITTED]

For an object interaction scenario specified as a labelled net, the location where an event occurs is represented by a transition and the location of a condition by a place. The semantic meanings of conditions and events are denoted by the labels of the places and transitions respectively. For an event to occur, some conditions must be fulfilled in advance and some afterwards. These pre-conditions and post-conditions are represented by the pre-set and post-set of the transition representing the event.

Step 1 of the proposed method is to specify the given object interaction scenarios as labelled nets with an AMG-structure. Consider an object-oriented system involving two objects, x and y, of classes X and Y respectively. There are three typical interaction scenarios exhibited by x and y, specified as UML sequence diagrams and collaboration diagrams (BRJ99, RJB99) in Figure 7. In conventional UML sequence diagrams and collaboration diagrams, there are no formal notations for denoting the pre-condition and post-condition of each event occurrence in an object interaction scenario. Therefore, for an explicit representation of the causal relationship between events and conditions, appropriate condition labels are appended to these diagrams.

[FIGURE 7 OMITTED]

Figure 8 shows object interaction Scenarios l, 2 and 3, specified as labelled nets ([N.sub.1], [M.sub.10]), ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]) respectively. They all are of AMG-structure.

([N.sub.1], [M.sub.10]) is constructed for representing scenario 1 as follows. For each location of a condition, a new place with a proper condition label is created. For example, [p.sub.11] denotes a location of condition [c.sub.11] for object x, so condition label x.[c.sub.11] is assigned to [p.sub.11]. For each event occurrence, a new transition with a proper event label is constructed. For example, [t.sub.11] denotes an occurrence of event [e.sub.1], so event label [e.sub.1] is assigned to [t.sub.11]. The event occurrence has a pre-condition x.[c.sub.11] and a post-condition x.[c.sub.12]. Hence, *[t.sub.11] = { [p.sub.11] } and [t.sub.11]* = { [p.sub.12] }. Arcs between [p.sub.11] (pre-condition) and [t.sub.11] and between [t.sub.11] and [p.sub.12] (post-condition) are appended for denoting their causal relationships. The rest locations of conditions and events are created accordingly. Following the same rules, ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]) are constructed for representing scenarios 2 and 3, respectively.

[FIGURE 8 OMITTED]

5 Synthesising and analysing the integrated system

After specifying the object interaction scenarios as augmented marked graphs (Step 1 of the proposed method), we synthesise these scenarios into an integrated system. In principle, a scenario portrays partial system behaviours of how the objects are interacted in order to perform a specific functionality. These augmented marked graphs are essentially partial system behavioural specifications which are to be synthesised together to form a single coherent whole.

This section describes Step 2 of our proposed method - the synthesis of labelled nets into an integrated net which represents the integrated system, and analysis of the system. The synthesis is based on the authors' earlier work on use-case-driven system design [38]. It is made by fusing those places with refer to the same system initial state or condition. The integrated net so obtained is of AMG-structure, so its liveness, boundedness, reversibility and conservativeness can be effectively analysed by making use of the special properties of augmented marked graphs.

Consider the labelled nets ([N.sub.1], [M.sub.10]), ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]) in Figure 8. Places [p.sub.11] in ([N.sub.1], [M.sub.10]), [p.sub.21] in ([N.sub.2], [M.sub.20]) and [p.sub.31] in ([N.sub.3], [M.sub.30]) refer to the same condition x.[c.sub.11]. Also, places [p.sub.15] in ([N.sub.1], [M.sub.10]), [p.sub.24] in ([N.sub.2], [M.sub.20]) and [p.sub.34] in ([N.sub.3], [M.sub.30]) refer to the same condition y.[c.sub.21]. Hence, [p.sub.11], [p.sub.21], and [p.sub.31] are fused into one place [p.sub.4l], and [p.sub.15], [p.sub.24] and [p.sub.34] into [p.sub.42].

Figure 9 then shows the integrated net (N, [M.sub.0]) obtained after synthesising ([N.sub.1], [M.sub.10]), ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]). (N, [M.sub.0]) is of an AMG-structure, meaning that it is structurally an augmented marked graph (N, [M.sub.0]; R), where R = {[p.sub.41], [p.sub.42]}.

[FIGURE 9 OMITTED]

For (N, [M.sub.0]; R), every R-siphon contains a marked place, and hence, would never become empty. According to Properties 3.2 and 3.3, (N, [M.sub.0]; R) is live and reversible. Since every place in its R-transform is covered by cycles, according to Property 3.4, (N, [M.sub.0]; R) is also bounded and conservative. Therefore, it can be concluded that the integrated system is well-behaved.

6 Eliminating duplicate labels from the integrated net

Consolidating the object interaction scenarios, the integrated net obtained from Step 2 of the proposed method serves to represent the system as a coherent integrated whole. In general, this integrated net is not necessarily uniquely labelled. For the integrated net (N, [M.sub.0]) in Figure 9 for example, places [p.sub.15] and [p.sub.26] have the same condition label y.[c.sub.22], and transitions [t.sub.13] and [t.sub.24] have the same event label [e.sub.3]. This reflects the fact that the locations or conditions for occurrence of the same event may be different at different moments within a scenario or among different scenarios. Yet, every condition is eventually implemented as a unique system substate and every event as a unique operation. Therefore, in order for the integrated net to be effectively used for implementation purposes, it need to be uniquely labelled where all the duplicate condition labels and duplicate event labels are eliminated.

The elimination cannot be done by just fusing places with the same condition label, and transitions with the same event label. This is because the resulting net may exhibit firing sequences different from the original ones. In other words, the system behaviours may be distorted. Step 3 of the proposed method is to eliminate all duplicate labels while preserving the original firing sequences (event sequences). This section describes this step in details.

Definition 6.1. Let S be a uniquely labelled subnet of a labelled net N. The pattern of S in N, denoted as Patt(N, S), is a condition-event net with an identical structure and label allocation as S while ignoring the identities of places and transitions of S.

Definition 6.2. Let [L.sub.x] and [L.sub.y] be patterns of subnets in a labelled net. [L.sub.x] [union] [L.sub.y] and [L.sub.x] [intersection] [L.sub.y] denote the union and intersection of [L.sub.x] and [L.sub.y], respectively. [L.sub.x] \ [L.sub.y] denotes the displacement of [L.sub.x] from [L.sub.y]. [L.sub.x] and [L.sub.y] are said to be disjoint if and only if [L.sub.x] [intersection][L.sub.y] = [empty set]

Definition 6.3. For a labelled net N, a uniquely labelled subnet S is called a common subnet if and only if there exists at least one uniquely labelled subnet S' such that S' [not equal to] S and Patt(N, S') = Patt(N, S). Let S be a pattern of the common subnets in N. [N, L] = { S | Patt(N, S) = L } represents the group of common subnets having the same pattern L.

Definition 6.4. For a subnet S = < F, T, F > of a PT-net, Pre(S) = (W) [union] (T'\P') is called the pre-set of S, Post(S) = (P*\T') [union] (T'*\P') is called the post-set of S, Head(S) = Pre(S)* [intersection] (P' [union] T') is called the head of S, and Tail(S) = *Post(S) [intersection] (P' [union] T') is called the tail of S.

Definition 6.5. A subnet S of a PT-net N = < P, T, F > is said to be of PP-type if and only if Head(S) [subset or equal to] P and Tail(S) [subset or equal to] P.

Figure 10 shows a uniquely labelled subnet S which is PP-type. Figure 11 shows the pattern of S.

[FIGURE 10 OMITTED]

[FIGURE 11 OMITTED]

We propose to eliminate duplicate labels by fusion of common subnets, as outlined below.

Identify groups of common subnets for fusion. These groups of common subnets need to be maximal and disjoint for two reasons. First, the net obtained after the fusion will become uniquely labelled. Second, the number of groups of common subnets for fusion can be reduced to minimum as they are maximal.

Transformation of common subnets. For preservation of firing sequences, common subnets are transformed before fusion. Based on coloured Petri nets [39], a unique colour is assigned to each common subnet as colour labels of its ingoing and outgoing arcs. A token flowing into the common subnet is coloured according to the colour label of the ingoing arc. Its colour is reset as it flows out via the same colour-labelled outgoing arc. Besides, the subnets are converted to PP-type.

Fusion of transformed common subnets. The transformed common subnets of each group are fused into a single subnet. A uniquely labelled net is ultimately obtained.

The following algorithm formally describes the elimination process. A detailed elaboration of the elimination process can be found in the authors' earlier work [40].

Elimination of Duplicate Labels from a Labelled Net

1. Identify maximal disjoint groups of common subnets :

1.1 Find all possible common subnets from N. Let J = { [L.sub.1], [L.sub.2], ..., [L.sub.n]} be their patterns.

1.2 Retain only the maximal patterns : Remove any U from 3 if there exists [L.sub.j] [member of] J such that [L.sub.i] is a sub-pattern of [L.sub.i] and [for all] [S.sub.i] [member of] [N, [L.sub.i]], [there exist] [S.sub.j] [member of] [N, [L.sub.j]]: [S.sub.i] is a subnet of [S.sub.j].

1.3 Make the overlapping patterns disjoint: For every [L.sub.i], [L.sub.j], [member of] J such that [L.sub.i] [not equal to] [L.sub.j] and J and [L.sub.i] are not disjoint, set J = (J - { [L.sub.i], [L.sub.j]}) [union] { [L.sub.i] [intersection] [L.sub.j]} [union] { [L.sub.i]\[L.sub.j],} [union] { [L.sub.j]\[L.sub.i]}.

1.4 Categorise the common subnets of N into groups { [N, [L.sub.i], [L.sub.i] [member of] J }.

2. For each group of common subnets [N, [L.sub.i]:

2.1 Convert each subnet S [member of] [N, [L.sub.i]] if S is not of PP-type:

2.1.1 For each transition [t.sub.i] [member of] Head(S) : (a) Create dummy transition [t.sub.i]' with unique label [[epsilon].sub.i], dummy place [p.sub.i]' with label [[psi].sub.i], and arcs ([t.sub.i]', [p.sub.i]') and ([p.sub.j]', [t.sub.i]). (b) For each p [member of] *[t.sub.i] : Remove arc (p, [t.sub.i]), and then create arc (p, [t.sub.i]'). (c) Re-define S by including [p.sub.i]' and ([p.sub.i]', [t.sub.i]).

2.1.2 For each transition [t.sub.j] [member of] Tails(S) : (a) Create dummy transition [t.sub.j]' with unique label [[epsilon].sub.j], dummy place [p.sub.j]' with label [[psi].sub.j], and arcs ([t.sub.j], [P.sub.j]') and ([p.sub.j]', [t.sub.j]'). (b) For each p [member of] [t.sub.j]* : Remove arc ([t.sub.j], p), and then create arc ([t.sub.j]', p). (c) Re-define S by including [p.sub.j]' and ([t.sub.j]', [p.sub.j]).

2.2 Assign a unique colour label [kappa] for each subnet S [member of] [N, [L.sub.i]]:

2.2.1 For each arc ([t.sub.i], [p.sub.i]) where [t.sub.i] [member of] Pre(S) and [p.sub.i] [member of] Head(S) : Assign colour label [kappa] to ([t.sub.i], [p.sub.i]).

2.2.2 For each arc ([p.sub.j], [t.sub.j]) where p [member of] Tail(S) and [t.sub.j] [member of] Post(S): Assign colour label [kappa] to ([p.sub.j], [t.sub.j]).

2.3 Fuse the common subnets in [N, [L.sub.j]] into one single subnet.

We apply the algorithm for eliminating the duplicate labels for the integrated net (N, [M.sub.0]) in Figure 9. Figure 12 shows the uniquely labelled net (N', [M.sub.0]') so obtained.

[FIGURE 12 OMITTED]

7 Obtaining object-Based behavioural specifications

In this section, we show Step 4 of our proposed method to obtain the individual object-based behavioural specifications. These individual object-based behavioural specifications are obtained by projecting the integrated net onto individual objects.

The projection is made by ignoring those places, transitions and arcs which are irrelevant to the object concerned. The projected net so obtained serves as the object behavioural specifications.

Consider the integrated net (N', [M.sub.0]') in Figure 12. The projection onto object x is obtained as follows. We keep those places with object label x (including dummy places) and those transitions (including dummy transitions) having at least one input place or output place labelled by x, as well as their associated arcs. Similarly, for the projection onto object y, we keep those places with object label y (including dummy places) and those transitions (including dummy transitions) having at least one input place or output place labelled by y, as well as their associated arcs.

Figure 13 shows the projections ([N.sub.x], [M.sub.x](l) and ([N.sub.y], [M.sub.y0]) obtained by projecting the net (N', [M.sub.0]') in Figure 12 onto objects x and y, respectively. ([N.sub.x], Mx0) and ([N.sub.y], [M.sub.y0]) are uniquely labelled, simply because (N1, [M.sub.0]') is uniquely labelled. They serve as the behavioural specifications for objects x and y, where conditions and events are uniquely represented.

8 Real-life example

This section presents a real-life example to further illustrate the refinement process.

[FIGURE 13 OMITTED]

The real-life example is an Office Access Control System. The system is briefly described as follows. It is a system used in a company for controlling staff accesses to its 30+ offices and laboratories. Among these offices and laboratories, some can be accessed by all staff while some others by authorised staff only and/or during specified time periods only. For controlling the staff access, every entrance is implemented with a card-reader, an emergency switch and an electronic lock, all being connected to a centralised server. The server maintains the access privileges and validates every access to the offices/laboratories. There are three typical cases for each request for access.

Authorised access ([U.sub.1]). A staff member wants to access an office/laboratory. He/She presents his/her staff card via a card-reader. Access is granted. The door is unlocked for five seconds and then re-locked.

Unauthorised access ([U.sub.2]). A staff member wants to access an office/laboratory. He/She presents his/her staff card via a card-reader. Access is not granted. The door is locked.

Emergency access ([U.sub.3]). A staff member wants to access an office/laboratory for emergency. He/She presses the emergency key. The door is unlocked immediately, until it is reset by a security officer.

From the object-oriented perspectives, the server (s : Server) and doors (d : Door) are objects of the Office Access Control System. They are interacting with each other in order to perform the above system functionalities. There are three object interaction scenarios, corresponding to [U.sub.1], [U.sub.2] and [U.sub.3].

Figure 14 shows these object interaction scenarios specified as UML sequence diagrams and collaboration diagrams, where appropriate condition labels are appended for denoting the pre-conditions and post-conditions for each event occurrence.

[FIGURE 14 OMITTED]

Step 1 of the proposed method is to specify object interaction scenarios as labelled nets. Figure 15 shows the labelled nets ([N.sub.1], [M.sub.10]), ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]) representing the object interaction scenarios for [U.sub.1], [U.sub.2] and [U.sub.3], respectively.

Step 2 of the proposed method is to synthesise the labelled net into an integrated system, and analyse the system on its liveness, boundedness, reversibility and conservativeness. ([N.sub.1], [M.sub.10]), ([N.sub.2], [M.sub.20]) and ([N.sub.3], [M.sub.30]) are synthesised into an integrated net (N, [M.sub.0]) by fusing those places which refer to the same system initial states or conditions : Places [p.sub.11], [p.sub.21] and [p.sub.31] are fused into one place [p.sub.41], and [p.sub.15], [p.sub.24] and [p.sub.34] into [p.sub.42]. Figure 16 shows the integrated net (N, [M.sub.0]) so obtained.

[FIGURE 15 OMITTED]

[FIGURE 16 OMITTED]

The integrated net (N, [M.sub.0]) is of an AMG-structure. Let R = { [p.sub.41], [p.sub.42] }. For (N, [M.sub.0]; R), every R-siphon contains a marked place and hence would never become empty. According to Properties 3.2 and 3.3, (N, [M.sub.0]; R) is live and reversible. Since every place in its R-transform is covered by cycles, according to Property 3.4, (N, [M.sub.0]; R) is also bounded and conservative. Therefore, it may be concluded that the Office Access Control System is well-behaved.

As shown in Figure 16, (N, [M.sub.0]) is not uniquely labelled as it contains duplicate labels. For example, place [p.sub.12] and [p.sub.22] have the same condition label s.[c.sub.12] and transitions [t.sub.11] and [t.sub.21] have the same event label et. Since every condition is eventually implemented as a unique substate and every event as a unique operation, in order for the integrated net to be effectively used for implementation purposes, these duplicate labels must be eliminated.

Step 3 of the proposed method is to eliminate duplicate condition labels and duplicate event labels from the integrated net (N, [M.sub.0]) through the fusion of common subnets. We perform this elimination process by applying the algorithm described in Section 6. Figure 17 shows the uniquely labelled net (N', [M.sub.0]') so obtained.

[FIGURE 17 OMITTED]

Step 4 of the proposed method is to obtain the individual object-based behavioural specification as projections of the integrated net onto the objects. The projection is made by ignoring those places, transitions and arcs which are irrelevant to the object concerned.

Consider the integrated net (N', [M.sub.0]') in Figure 17. For the projection onto object s (the server object), we keep those places with object label s (including dummy places) and those transitions (including dummy transitions) having at least one input place or output place labelled by s, as well as their associated arcs. Similarly, for the projection onto object d (the door object), we keep those places with object label d (including dummy places) and those transitions (including dummy transitions) having at least one input place or output place labelled by d, as well as their associated arcs. Figure 18 shows the projections ([N.sub.s], [M.sub.s0]) and ([N.sub.d], [M.sub.d0]) obtained by projecting the integrated net (N', [M.sub.0]') in Figure 17 onto objects s and d, respectively.

[FIGURE 18 OMITTED]

As the integrated net (N', [M.sub.0]') is uniquely labelled, its projections ([N.sub.s], [M.sub.s0]) and ([N.sub.d], [M.sub.d0]) are also uniquely labelled, where every condition or event is uniquely represented. ([N.sub.s], [M.sub.s0]) and ([N.sub.d], [M.sub.d0]) then serve as the behavioural specifications for the server (s : Server) and door (d : Door) objects, respectively.

9 Conclusion

One of the most difficult tasks in object-oriented system design is to obtain individual object-based behavioural specifications from a given set of object interaction scenarios. Not only conventional specification constructs for object interaction scenarios are too primitive to represent the partial ordering of events and the causal relationship between the events and conditions, there also involves different abstractions between intra-object lifecycle and inter-object interaction. Moreover, we have to ensure that the derived object-based behavioural specifications reflect exactly the given object interaction scenarios and that the system is well-behaved.

We proposed a Petri-net-based method for refining a given set of object interaction scenarios into individual object-based behavioural specifications. By specifying the object interaction scenarios as labelled nets with an AMG-structure and synthesising them into an integrated net, we analyse the system, based on the special properties of augmented marked graphs. For unique representation of events and conditions, an algorithm is applied to the integrated net to eliminate duplicate condition labels and event labels while preserving the event sequences. Object-based behavioural specifications are then obtained as projections of the integrated nets onto the objects. The whole refinement process has been described, elaborated and illustrated using the Office Access Control System example.

The proposed method offers a number of distinctive features. First, object interaction scenarios are formally specified as labelled nets which are unambiguous and semantically rich for an explicit representation of events, conditions and their causal relationships. Second, object-based behavioural specifications are rigorously derived from the given object interaction scenarios through systematic synthesis and projection. The behavioural specifications so obtained would reflect exactly the given object interaction scenarios. Third, liveness, boundedness, reversibility and conservativeness of the system can be effectively analysed by making use of the special properties of augmented marked graphs. Fourth, every event or condition is uniquely represented in the behavioural specifications so that the specifications can be readily used for implementation purposes.

With a strong theoretical foundation of Petri nets, the proposed method can be effectively used for refining object-based behavioural specifications from a set object interaction scenarios. It resolves a number of problems perplexing the designers of object-oriented systems, such as the lack of formality in specifying object interaction scenarios and the difficulty of ensuring the correctness of object behavioural specifications. The latter is especially important for systems involving shared resources, where erroneous situations such as deadlock and capacity overflow are easily induced. The proposed method can be implemented as tool to support object-oriented system design. By capturing the functional requirements of a system as a set of object interaction scenarios, it helps perform rigorous system synthesis and analysis. The correctness of this refinement can be assured. Moreover, the object-based behavioural specifications so obtained can be readily used for code generation. This inevitably contributes towards a smooth transitions from functional requirements through design to implementation for object-oriented system development.

Received: April 12, 2008

References

[1] J. Iivari (1995), "Object Orientation as Structural, Functional and Behavioural Modelling : A Comparison of Six Methods for Object-Oriented Analysis", Information and Software Technology, Vol. 37, No. 3, pp. 155-163.

[2] K.S. Cheung and K.O. Chow (1996), "Comparison of Object-Oriented Models by Views and Abstraction Constructs", Proceedings of the International Conference on Intelligent Technologies in Human-Related Sciences, pp. 335342, Leon, Spain.

[3] K.O. Chow and S. Yeung (1996), "Behavioural Modelling in Object-Oriented Methodologies", Information and Software Technology, Vol. 38, No. 10, pp. 657-666.

[4] K.S. Cheung, K.O. Chow and T.Y. Cheung (1997), "A Feature-Based Approach for Consistent Object-Oriented Requirements Specifications". W.G. Wojtkowshi et al. (eds.), Systems Development Methods for the Next Century, pp. 31-38, Plenum Publishing.

[5] K.S. Cheung, K.O. Chow and T.Y. Cheung (1999), "Extending Formal Specification to Object Oriented Models Through Level-View Structured Schemas". J. Chen, J. Lu and B. Meyer (eds.), Technology of Object Oriented Languages and Systems, Vol. 31, pp. 118-125, IEEE Computer Society Press.

[6] B. Breu et al. (1998), "Systems, Views and Models of UML". M. Schader and A. Korthaus (eds.), The Unified Modeling Language : Technical Aspects and Applications, Physica- Verlag.

[7] G. Booch, J. Rumbaugh and I. Jacobson (1999), The Unified Modeling Language : User Guide, Addison-Wesley.

[8] J. Rumbaugh, I. Jacobson and G. Booch (1999), The Unified Modeling Language : Reference Manual, Addison-Wesley.

[9] I. Graham et al. (2001), Object-Oriented Methods : Principles and Practice, Addison-Wesley.

[10] I. Jacobson et al. (1992), Object-Oriented Software Engineering : A Use-Case-Driven Approach, Addison-Wesley.

[11] I. Jacobson, G. Booch and J. Rumbaugh (1999), The Unified Software Development Process, Addition Wesley.

[12] G. Schneider and LP. Winters (1998), Applying Use Cases, Addison-Wesley.

[13] P. Kruchten (1999), The Rational Unified Process : An Introduction, Addison-Wesley.

[14] D. Rosenberg (1999), Use Case Driven Object Modeling with UML : A Practical Approach, Addison-Wesley.

[15] D. Rosenberg and K. Scott (2001), Applying Use Case Driven Object Modeling with UML, Addison-Wesley.

[16] J. Arlow and I. Neustadt (2002), UML and the Unified Process : Practical Object-Oriented Analysis and Design, Addison-Wesley.

[17] S. Kirani and W.T. Tsai (1994), "Method Sequence Specification and Verification of Classes", Journal of Object-Oriented Programming, Vol. 7, No. 6, pp. 28-38.

[18] K.S. Cheung, K.O. Chow and T.Y. Cheung (1998), "Consistency Analysis on Lifecycle Model and Interaction Model". C. Rolland and G. Grosz (eds.), Object-Oriented Information Systems, pp. 427-441, Springer.

[19] K.S. Cheung, K.O. Chow and T.Y. Cheung (1998), "Deriving Scenarios of Object Interaction through Petri Nets". J. Chen et al. (eds.), Technology of Object Oriented Languages and Systems, Vol. 27, pp. 118-125, IEEE Computer Society Press.

[20] M. Glinz (2000), "A Lightweight Approach to Consistency of Scenarios and Class Models", Proceedings of the IEEE International Conference on Requirements Engineering, pp. 49-58, IEEE Computer Society Press.

[21] F. Bordeleau and R.J.A. Buhr (1997), "UCMROOM Modelling : From Use Case Maps to Communicating State Machines", Proceedings of the IEEE International Symposium and Workshop on Engineering of Computer-Based Systems, pp. 169-178, IEEE Computer Society Press.

[22] F. Bordeleau, J.P. Corriveau and B. Selic (2000), "A Scenario-Based Approach to Hierarchical State Machine Design", Proceedings of the International Symposium on Object-Oriented Real-Time Distributed Computing, pp. 78-85, IEEE Computer Society Press.

[23] B. Dano, H. Briand and F. Barbier (1996), "Progressing Towards Object-Oriented Requirements Specifications Using the Use Case Concept", Proceedings of the IEEE Symposium and Workshop on Engineering of Computer-Based Systems, pp. 450-456, IEEE Computer Society Press.

[24] B. Dano, H. Briand and F. Barbier (1997), "An Approach Based on the Concept of Use Case to Produce Dynamic Object-Oriented Specifications", Proceedings of the IEEE International Symposium on Requirements Engineering, pp. 54-64, IEEE Computer Society Press.

[25] P. Graubmann (1988), "The Construction of EN Systems from a Given Trace Behaviour", Advances in Petri Nets, Lecture Notes in Computer Science, Vol. 340, pp. 133-153, Springer-Verlag.

[26] E. Smith (1991), "On Net Systems Generated by Process Foldings", Advances in Petri Nets, Lecture Notes in Computer Science, Vol. 524, pp. 253-295, Springer-Verlag.

[27] K. Hiraishi (1992), "Construction of a Class of Safe Petri Nets by Presenting Firing Sequences", Application and Theory of Petri Nets, Lecture Notes in Computer Science, Vol. 616, pp. 244-262, Springer-Verlag.

[28] W.J. Lee, S.D. Cha and Y.R. Kwon (1998), "Integration and Analysis of Use Cases Using Modular Petri Nets in Requirement Engineering", IEEE Transactions on Software Engineering, Vol. 24, No. 12, pp. 1115-1130.

[29] J.L. Peterson (1981), Petri Net Theory and the Modelling of System, Prentice Hall.

[30] W. Reisig (1985), Petri Nets : An Introduction, Springer-Verlag.

[31] T. Murata (1989), "Petri Nets : Properties, Analysis and Applications". Proceedings of the IEEE, Vol. 77, No. 4, pp. 541-580.

[32] J. Desel and W. Reisig (1998), "Place Transition Petri Nets", Lectures on Petri Nets I : Basic Models, Lecture Notes in Computer Science, Vol. 1491, pp. 122-173, Springer-Verlag.

[33] J. Desel and J. Esparza (1995), Free-choice Petri Nets, Cambridge University Press.

[34] F. Chu and X. Xie (1997), "Deadlock Analysis of Petri Nets Using Siphons and Mathematical Programming", IEEE Transactions on Robotics and Automation, Vol. 13, No. 6, pp. 793-804.

[35] K.S. Cheung (2004), "New Characterisations for Live and Reversible Augmented Marked Graphs", Information Processing Letters, Vol. 92, No. 5, pp. 239-243.

[36] K.S. Cheung and K.O. Chow (2005), "Cycle Inclusion Property of Augmented Marked Graphs", Information Processing Letters, Vol. 94, No. 6, pp. 271-276.

[37] K.S. Cheung (2007), "Liveness and Boundedness of Augmented Marked Graphs", IMA Journal of Mathematical Control and Information, Vol. 24, No. 2, pp. 235-244.

[38] K.S. Cheung, T.Y. Cheung and K.O. Chow (2006), "A Petri-Net-Based Synthesis Methodology for Use-Case-Driven System Design", Journal of Systems and Software, Vol. 79, No. 6, pp. 772-790.

[39] K. Jensen (1986), "Coloured Petri Nets", Petri Nets : Central Models and Their Properties, Lecture Notes in Computer Science, Vol. 254, pp. 248-299, Springer-Verlag.

[40] K.S. Cheung and K.O. Chow (2006), "Elimination of Duplicate Labels in Petri-Net-Based System Specification", Proceedings of the International Conference on Computer and Information Technology, pp. 932-936, IEEE Computer Society Press.

King-Sing Cheung

University of Hong Kong 

Pokfulam, Hong Kong 

E-mail : [e-mail]

City University of Hong Kong 

Tat Chee Avenue, Hong Kong

E-mail : [e-mail]

(1) This paper is an extended version of the authors' paper presented at the REFINE 2006 workshop.