Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols

Ansgar Fehnker, Matthias Fruth, Annabelle McIver

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

13 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationMethods, Models and Tools for Fault Tolerance
EditorsMichael Butler, Cliff Jones, Alexander Romanovsky, Elena Troubitsyna
Place of PublicationBerlin
PublisherSpringer
Pages1-24
Number of pages24
ISBN (Electronic)978-3-642-00867-2
ISBN (Print)978-3-642-00866-5
DOIs
Publication statusPublished - 2009
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume5454
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Wireless networks
Network protocols
Computer simulation
Model checking
Telecommunication links
Specifications
Topology

Keywords

  • Complexity
  • Design
  • Formal Method
  • Modeling
  • System development
  • Validation
  • Verification

Cite this

Fehnker, A., Fruth, M., & McIver, A. (2009). Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. In M. Butler, C. Jones, A. Romanovsky, & E. Troubitsyna (Eds.), Methods, Models and Tools for Fault Tolerance (pp. 1-24). (Lecture Notes in Computer Science; Vol. 5454). Berlin: Springer. https://doi.org/10.1007/978-3-642-00867-2_1
Fehnker, Ansgar ; Fruth, Matthias ; McIver, Annabelle. / Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. Methods, Models and Tools for Fault Tolerance. editor / Michael Butler ; Cliff Jones ; Alexander Romanovsky ; Elena Troubitsyna. Berlin : Springer, 2009. pp. 1-24 (Lecture Notes in Computer Science).
@inbook{eb5ec1ebacc348d195b4a0e72dd11df3,
title = "Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols",
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.",
keywords = "Complexity, Design, Formal Method, Modeling, System development, Validation, Verification",
author = "Ansgar Fehnker and Matthias Fruth and Annabelle McIver",
year = "2009",
doi = "10.1007/978-3-642-00867-2_1",
language = "English",
isbn = "978-3-642-00866-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--24",
editor = "Michael Butler and Cliff Jones and Alexander Romanovsky and Elena Troubitsyna",
booktitle = "Methods, Models and Tools for Fault Tolerance",

}

Fehnker, A, Fruth, M & McIver, A 2009, Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. in M Butler, C Jones, A Romanovsky & E Troubitsyna (eds), Methods, Models and Tools for Fault Tolerance. Lecture Notes in Computer Science, vol. 5454, Springer, Berlin, pp. 1-24. https://doi.org/10.1007/978-3-642-00867-2_1

Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. / Fehnker, Ansgar ; Fruth, Matthias; McIver, Annabelle.

Methods, Models and Tools for Fault Tolerance. ed. / Michael Butler; Cliff Jones; Alexander Romanovsky; Elena Troubitsyna. Berlin : Springer, 2009. p. 1-24 (Lecture Notes in Computer Science; Vol. 5454).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols

AU - Fehnker, Ansgar

AU - Fruth, Matthias

AU - McIver, Annabelle

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

KW - Complexity

KW - Design

KW - Formal Method

KW - Modeling

KW - System development

KW - Validation

KW - Verification

U2 - 10.1007/978-3-642-00867-2_1

DO - 10.1007/978-3-642-00867-2_1

M3 - Chapter

SN - 978-3-642-00866-5

T3 - Lecture Notes in Computer Science

SP - 1

EP - 24

BT - Methods, Models and Tools for Fault Tolerance

A2 - Butler, Michael

A2 - Jones, Cliff

A2 - Romanovsky, Alexander

A2 - Troubitsyna, Elena

PB - Springer

CY - Berlin

ER -

Fehnker A, Fruth M, McIver A. Graphical Modelling for Simulation and Formal Analysis of Wireless Network Protocols. In Butler M, Jones C, Romanovsky A, Troubitsyna E, editors, Methods, Models and Tools for Fault Tolerance. Berlin: Springer. 2009. p. 1-24. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-00867-2_1