Stochastic Modelling of Communication Protocols from Source Code

A major development in qualitative model checking was the jump to verifying properties of source code directly, rather than requiring a separately specified model. We describe and motivate similar extensions to quantitative / performance analyses, with particular emphasis on communication protocols. The central aim is to extract a stochastic model (in the PEPA language) from such source code. We construct a model compositionally, so that each function in the system corresponds to a sequential PEPA process. Such a process is derived by abstract interpretation over the state machine of a function, using interval abstraction to represent linear expressions of integer variables. We illustrate this by an analysis of a simple protocol.