Modelling and analysis of distributed software using GSPNs

This chapter discusses the role that Generalized Stochastic Petri Nets (GSPN) can play in the static analysis of distributed software. The material is organized along two main lines: the need and the advantages of studying both qualitative and quantitative aspects of a program, and the need for doing it in an automatic manner. The role of performance evaluation in the analysis of distributed software is illustrated through a small example, classical in the qualitative approach (the dining philosophers). Although small this example allows to point out the need and the requirements of automatic translation and to discuss the main hypothesis behind program performance evaluation through GSPN models. A procedure for the automatic generation of GSPN models starting from a distributed program written in a CSP-like language, and for the definition of program performance indices in terms of GSPN ones is then given and illustrated by means of a realistic example.