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 Such a process is derived by abstract interpretation over the state machine of a function, using abstraction to represent linear expressions of integer variables. We illustrate this by an analysis of a simple protocol.

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Michael J. A. Smith
• Keywords: ENTCS 2007, Model, Qualitative Model, Source Code