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

10

MODELLING AND
ANALYSIS OF
CONC U RRENT
PROGRAMS

In this chapter we provide an example of how GSPNs can be used to evaluate
and validate concurrent programs. Parallel programs are translated into
GSPN models that are used to perform a static analysis yielding information
on possible deadlocks, mutual exclusion, and resource utilization, as well as a
dynamic analysis to study performance. These models help understand the
overall behaviour of a concurrent program, to increase the confidence in its
correctness, and assess the e ciency of its implementation. The example of
this chapter shows a class of GSPN models that do not require any ingenuity
from the modeller to be built, as they are obtained through an automatic
translation process.
The usefulness of Petri net models for the static analysis of concurrent pro-
grams was pointed out in [70] for programs written in languages such as
Ada [ 62] , Occam [23] and others, while relations between Petri nets and
other concurrent languages and paradigms such as CCS [49] and CSP [ 32]
have been widely studied in the literature [ 29] .

10.1 Introduction to the Static Analysis of Con-

current Programs

Static analysis is a method that draws conclusions on the qualitative be-
haviour of a program by “simply” looking at its code without requiring any
execution (that is to say, at compile time). The classical approach of static
analysis is to derive from the program a formal model that is subsequently

241