6 Model validation

Model validation means

• Correctness validation
• Performance validation

The first can be undertaken by simulation and by using the analysis tools: reachability three and invariants. For the second, simulation is the tool to use.

We will demonstrate model development and validation on a small but realistic application.

6.1 A seat-reservation system

The example is taken from [Reisig 1985]. The seat-reservation system is originally developed and described as an inscribed net. Part of the net is then successively transformed into a P/T-net. This net can be analyzed by running it with some Petri net tool like SimNet. It can also be analyzed by deriving place invariants.

From the invariant analysis we have

    1      Kµ(x) + µ(y)  + µ(k) + µ(k') = K
    2      µ(y)  + µ(k') + µ(P) + µ(q)  = K
    3      µ(x)  + Lµ(y) + µ(W) + µ(W') = L
    4      Kµ(x) + µ(k)                 = µ(P) + µ(q)

where the fourth invariant has been obtained by adding 1 and 2.

From 2 we obtain

   µ(P) = K - (µ(y) + µ(k') + µ(q)) =< K

i.e., P cannot be overbooked (P₁ = property 1, Reisig).

Point 4 and µ(x) = 1 gives

    µ(P) + µ(q) = K + µ(k) = K

i.e., when µ(P) + µ(q) = K, reservation goes to the waiting list as it should (P₂).

If W is nonempty, then µ(P) + µ(q) = K. From 2 we have then that µ(y) + µ(k') = 0, or µ(y) = µ(k') = 0, so that then a new booking cannot go to P, see Figure 78. If W and q are nonempty this means that the next booking must come by transfer from W until W is empty (P₃).