Analyzer in OOMPNets, OOMPOA

To analyze OOMPNets, there are four steps to achieve. The first one transforms the OOMPNet into T-CPN with a transformation algorithm. Secondly, user constructs the occurrence graph of the T-CPN. This step can be done automatically, too. The third step uses the built occurrence graph to investigate dynamic properties, e.g.

liveness property, home property and so on. According the results of the investigated dynamic properties, the error(s) embedded in the T-CPN can be found. The forth step maps the found errors to the original OOMPNet. Figure 5-9 and 5-10 show the T-CPN transformed from the OOMPNet of scenario “transfer account successfully” and the

61

occurrence graph respectively. The T-CPN contains an index table which maps the transformed complex token in OOMPNet to the transformed places of the corresponding object-net. The red arcs in the T-CPN are arcs of OOTPA described in Sec. 4.1. The transitions in the T-CPN are corresponding to the groups of STG. So, the label of each transition in the T-CPN is the format of the groups in STG. For example, the transition {(System manager turn on ATM,Machineatm),Turn on} in the T-CPN is generated by grouping the bct of transition System manager turn on ATM and the transition Turn on in the object-net atm.

The bct is Machineatm where Machine is complex type variable and atm is the name of the complex token. The occurrence graph in Figure 5-10 is a direct graph.

Vertices in occurrence graph are representing the reachable markings of the T-CPN.

The format of markings is (multi-set of tokens in place 1; multi-set of tokens in place 2; …; multi-set of tokens in place n) where n is the number of places in the T-CPN. A complex token is represented by the marking of the corresponding object-net according to the index table. Because the format of markings is too long, the code names are used to represent markings instead. For example, (1) in Figure 5-10 represents the marking (( ; ; ),a   controller u; ; ; ; ; ; ; ; ; )        and so on. An edge in occurrence graph means a transition fired associated with a binding. The format of steps is (transition binding element, ) . For example, step3

({(Input password,Machineatm )}, User u ) fires the transition Input password and the binding element is <User=u>.

62

Figure 5-9 T-CPN of OOMPNet in Figure 5-5.

Figure 5-10 The occurrence graph of T-CPN in Figure 5-9.

63

Now the occurrence graph is analyzed to calculate four dynamic properties, best integer bounds, best multi-set bounds, liveness and home properties. According to the dynamic properties described in [1] and [2], Figures 5-11~5-14 show the results of the investigated dynamic properties.

Figure 5-11 The best integer bounds of the T-CPN.

Figure 5-11 shows the best integer bounds of the T-CPN. It contains two kinds, best upper integer bounds and best lower integer bounds. The best upper integer bound of a place specifies the maximum number of tokens associated with the place in any reachable markings. The upper integer bound of place Start is 2 which means place Start has at most 2 tokens, and there is at least one reachable marking whose place Start has 2 tokens too. Similarly, the lower integer bound of a place specifies the minimum number of tokens associated with the place in any reachable markings. The lower integer bound of place Start is 0 which means that there is at least zero token associated with place Start and there exists a reachable marking where there is no

64

token associated with place Start. A similar remark applies to other places.

Best Upper Multi-set Bounds

Figure 5-12 The best multi-set bounds of the T-CPN.

Above paragraph describes the best integer bounds of a place which ignores the token colors. Figure 5-12 shows the best upper and lower multi-set bounds of places.

65

It considers not only the number of tokens but also the colors of tokens. The best upper multi-set bound of a place specifies all possible multi-sets of token colors associated with the place where the sum of the coefficient of colors in each multi-set is equal to the best upper integer bound of the place. For example, the best upper multi-set bound of place Start has only one possible multi-set, 1’atm+1’u, where the sum of coefficient of colors in the multi-set is equal to the best upper integer bound of the place. It means that there exist reachable markings where one atm and one u are associated with place Start. Similarly, the best lower multi-set bound of a place specifies all possible multi-sets of token colors associated with the place where the sum of the coefficient of colors in each multi-set is equal to the best lower integer bound of the place. For example, the best lower multi-set bound of place Start is empty where the sum of coefficient of colors is 0 equal to the best lower integer bound of place Start. It means that there exists a reachable marking where there is no token associated with place Start. A similar remark applied to other places.

Home Properties

Home Markings: (6)

Figure 5-13 The home properties of the T-CPN.

Figure 5-13 shows the home properties of the T-CPN. The home properties show that there exists a single home marking, (6). Home marking means that all reachable markings can reach to the home marking. In other words, it is impossible to have an occurrence sequence which cannot be extended to reach the home marking [1].

66 transition cannot be enabled in any reachable markings. A transition is a live transition if and only if the transition is enabled in any reachable markings. The liveness properties of the T-CPN above are shown in Figure 5-14. There is a single dead marking (6) specified in Figure 5-14. There are four dead transitions in the T-CPN.

Finally, there are no live transitions.

According to the above investigated dynamic properties, developer traces to find out errors which are embedded in net elements. The OOT-Property arcs connect to transition {(Input account number,Machineatm)} cause transition {(Input account number,Machineatm)} to be unfirable. OOT-Property arcs are transformed from the complex type guard expression of transitions. And, transition {(Input account number,Machineatm)} corresponding to the group in STG is grouped from the transition Input account number in original OOMPNet. So, developer can check the guard expression of transition Input account number to find out errors. It finds that the guard expression Machine ( ; ; )a  in transition Input account number is an error inscription. The error inscription causes the transition and the following transitions to be dead transitions.

67