GSPN BASICS - Modelling with Generalised Stochastic Petri Nets - page 104

association of weights with immediate transitions requires only the informa-
tion about ECSs, not about reachable markings. For each ECS the analyst
thus defines a local association of weights from which probabilities are then
derived.

5.5 An Example of a GSPN Model

In this section we illustrate an example of the application of the GSPN
methodology to the modelling of systems.
Several steps must be followed in the study of a system with the GSPN
approach:

1. the model must be constructed, possibly using a structured technique,
either top-down or bottom-up, depending on the system to be mod-
elled;

2. the model must then be validated using the results of the structural
analysis, possibly formally proving some behavioural properties of the
model;

3. the performance indices of interest must be defined in terms of GSPN
markings and of transition firings;

4. the reachability set and the reachability graph must then be generated,
to obtain the continuous-time Markov chain associated with the GSPN
system;

5. the Markov chain must be solved;

6. the performance indices must be computed from the Markov chain
solution.

All steps must be performed with a suitable software tool that provides the
GSPN modelling environment, allowing the graphical creation and modi-
fication of a model, the definition of performance indices, the structural
analysis, and the stochastic analysis of the model.
In this chapter we only provide an example of a GSPN model, but in the
second part of the topic, after the analysis of GSPN models will be discussed
(this is the topic of the next chapter), the various steps of the modelling
process are illustrated.
The example that we illustrate next is obtained with a modification of the
standard readers & writers model. Actually, the GSPN model that we use,
which is depicted in Fig. 5.3, results from a further complication of the
model presented in Fig. 4.1 as an example of a PN model with priority. The
new feature introduced in the model is a local area network (LAN) transfer
phase that follows each read or write access to the shared memory.