MODELLING AND ANALYSIS OF CONCURRENT PROGRAMS - Modelling with Generalised Stochastic Petri Nets - page 228

studied to infer the properties of the program. Since during static anal-
ysis nothing is known about the run-time behaviour of the program (for
example its input data), no assumption is made about which of the pos-
sible execution paths is actually followed by the program. Static analysis
thus tends to account also for many program behaviours that would never
occur in real executions, but all possible run time behaviours are surely
included. Three types of anomalies may be detected by static analysis in
a distributed/concurrent environment [1] : unconditional faults, conditional
faults, and nonfaults. Unconditional faults correspond to errors that will
definitely occur during program executions. Conditional faults represent in-
stead errors whose occurrence depends either on nondeterministic choices
or on specific sets of input data. Nonfaults, finally, are errors which are re-
ported by the static analyser although they will never occur during program
executions: nonfaults are detected when the correct behaviour of programs
is ensured by control variables that are ignored during static analysis. Static
analysis thus provides a pessimistic picture of program behaviour: a mea-
sure of goodness of a static analyser is its ability to eliminate (or at least to
reduce) the number of nonfaults.
Once a concurrent program is determined to be correct it must also be fast.
A common way of analysing the performance of concurrent programs is to
construct appropriate queuing network models of the application, which ac-
count for the structure of the program and of the hardware of the application
and in which parameters and delay centres are carefully chosen to charac-
terize the application being modelled. This approach requires considerable
ingenuity. Moreover little relation exists between these models and those
used for validation purposes.
GSPNs can be considered as a formalism capable of representing both the
characteristics of the architecture (the hardware) and the peculiarities of the
program (the software) of a concurrent computer in such a way that both
validation and performance evaluation can be performed using basically the
same model. In principle, GSPNs can thus be used to prove the correctness
of a concurrent program as well as the e ciency of its implementation: for
an example the reader may refer to [8] , where a mutual exclusion algorithm
is first proved correct and subsequently evaluated to characterize the range
of applications for which it can be considered e cient. It is often the case,
however, that a complete assessment of the correctness and of the e ciency
of a program is not feasible with theoretical/analytical approaches, due to
the dimension of the state space. In these cases, GSPNs still play a relevant
role, as they allow the programmer to reason about program behaviours
using a formal specification, and making objective statements about their
properties and about their performances. In these cases the simulation of
the evolution of the model is particularly important. Indeed, GSPN mod-
els can aid the user in visualizing the many possible execution sequences of
the program. Being able to actually see the dynamic behaviour of a con-