Abstract
It is well-known that the performance of wireless protocols depends on the quality of the wireless links, which in turn is affected by the network topology. The aim of this paper is to investigate the use of probabilistic model checking in the analysis of performance of wireless protocols, using a probabilistic abstraction of wireless unreliability.
Our main contributions are first, to show how to formalise wireless link unreliability via probabilistic behaviour derived from the current best analytic models [12], and second, to show how such formal models can be generated automatically from a graphical representation of the network, and analysed with the PRISM model checker.
We also introduce CaVi, a graphical specification tool, which reduces the specification task to the design of the network layout, and provides a uniform design interface linking model checking with simulation. We illustrate our techniques with a randomised gossiping protocol.
Our main contributions are first, to show how to formalise wireless link unreliability via probabilistic behaviour derived from the current best analytic models [12], and second, to show how such formal models can be generated automatically from a graphical representation of the network, and analysed with the PRISM model checker.
We also introduce CaVi, a graphical specification tool, which reduces the specification task to the design of the network layout, and provides a uniform design interface linking model checking with simulation. We illustrate our techniques with a randomised gossiping protocol.
Original language | English |
---|---|
Title of host publication | Methods, Models and Tools for Fault Tolerance |
Editors | Michael Butler, Cliff Jones, Alexander Romanovsky, Elena Troubitsyna |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 1-24 |
Number of pages | 24 |
ISBN (Electronic) | 978-3-642-00867-2 |
ISBN (Print) | 978-3-642-00866-5 |
DOIs | |
Publication status | Published - 2009 |
Externally published | Yes |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 5454 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Keywords
- Complexity
- Design
- Formal Method
- Modeling
- System development
- Validation
- Verification