Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423879 | Electronic Notes in Theoretical Computer Science | 2007 | 17 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics