-
Using Process Algebra to Design Better Protocols.
Lero, Limerick, Ireland. November 2017.
abstract | pdf
Abstract:
Protocol design, development and standardisation still follow the lines of rough consensus and running code. This approach yields fast and impressive results in a sense that protocols are actually implemented and shipped, but comes at a price: protocol specifications, which are mainly written in natural languages without presenting a formal specification, are (excessively) long, ambiguous, underspecified and erroneous. These shortcomings are neither new nor surprising, and well documented. It is the purpose of this talk to provide further evidence that formal methods in general and process algebras in particular can overcome these problems. They provide powerful tools that help to analyse and evaluate protocols, already during the design phase. To illustrate this claim, I report how a combination of pen-and-paper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc On-Demand Vector (AODV) routing protocol.
-
Forwards and Backwards in Separation Algebra.
IFIP WG 2.1, Lesbos, Greece. October 2017.
abstract | pdf
Abstract:
In this talk I present a framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new operator, which I introduce. We implemented the framework in the interactive theorem prover Isabelle/HOL, and enable automation with several interactive proof tactics. I will end the presentation with a couple of open problems we are working on right now.
-
Verifying Liveness Properties: Assumptions and Problems.
IFIP WG 2.3, Mooloolaba, Australia. July 2017.
pdf
Abstract:
-
Forwards and Backwards in Separation Algebra.
University of Queensland, Brisbane, Australia. June 2017.
abstract | pdf
Abstract:
Separation algebra is a formal and abstract algebraic framework to describe separation logic. So far separation algebra was mainly used as an abstract base to reason about heaps. I will present an algebraic framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation algebra; and hence also for separation logic. While the former is well understood, the later requires the introduction of a new operator. Since this is work in progress I will point at some surprising algebraic problems that need to be solved within the setting of forward reasoning.
-
Split, Send, Reassemble: A Formal Specification of a CAN bus Protocol Stack"location: "Uppsala, Sweden.
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), April 2017.
abstract | pdf
Abstract:
We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an in-built mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
-
Using Process Algebra to Design Better Protocols.
University of Twente, The Netherlands. February 2017.
abstract | pdf
Abstract:
"Despite the maturity of formal description languages and formal methods for analyzing them, the description of real protocols is still overwhelmingly informal. The consequences of informal protocol description drag down industrial productivity and impede research progress" Pamela Zave\n This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying protocols.\n After a short introduction of “failures” in specifying protocols, I will give a brief overview of our work in this area, which includes the development of a process algebra for wireless protocols, and its application to prove loop freedom of the AODV routing protocol, one of the major protocols in the area of wireless mesh networks. The latter required some adaptations to the specification, as the original specification protocol was not loop free.\n I will show that our modular proof strategy makes it easy to check that crucial correctness properties, such as loop freedom, are preserved under changes in the specification. Through automatic translation from process-algebraic specifications into the input language of model checkers, such as UPPAAL, proposed specifications can be tested on the fly model-checking techniques.
-
Using Process Algebra to Design Better Protocols.
Vrije Universiteit Amsterdam, The Netherlands. January 2017.
abstract | pdf
Abstract:
"Despite the maturity of formal description languages and formal methods for analyzing them, the description of real protocols is still overwhelmingly informal. The consequences of informal protocol description drag down industrial productivity and impede research progress" Pamela Zave\n This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying protocols.\n After a short introduction of “failures” in specifying protocols, I will give a brief overview of our work in this area, which includes the development of a process algebra for wireless protocols, and its application to prove loop freedom of the AODV routing protocol, one of the major protocols in the area of wireless mesh networks. The latter required some adaptations to the specification, as the original specification protocol was not loop free.\n I will show that our modular proof strategy makes it easy to check that crucial correctness properties, such as loop freedom, are preserved under changes in the specification. Through automatic translation from process-algebraic specifications into the input language of model checkers, such as UPPAAL, proposed specifications can be tested on the fly model-checking techniques.
-
Statistical Model Checking with Uppaal.
NICTA, Sydney, Australia. December 2013.
abstract | pdf
Abstract:
This talk is a continuation of Franck's talk. Model Checking was successfully applied to countless (industrial) case studies, as Franck pointed out. However, several case studies indicate that model checking is limited in some scenarios: state space explosion restricts applicability to large distributed systems, and quantitative reasoning, often sufficient for applications, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this talk I will give a short introduction to statistical model checking and illustrate its usefulness by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, I will report on experiments where we pushed the limits of statistical model-checking and showed that this technology is capable of analysing networks of up to 100 nodes.
-
Formal Methods for Wireless Mesh Networks.
Argentina. August 2013.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the 'time-to-market' for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present how formal methods can be applied. In particular I will presents techniques used for modelling, analysing and verifying the Ad-hoc on Demand Distance Vector (AODV) routing protocol, one of the leading protocols for WMNs. The techniques includes a formal model using process algebra, fully automation by a matrix model and the use of (statistical) model checkers.
-
Topology-based Mobility Models for Wireless Networks.
Quantitative Evaluation of Systems (QEST'13), Buenos Aires, Argentina. August 2013.
abstract | pdf
Abstract:
The performance and reliability of wireless network protocols heavily depend on the network and its environment. In wireless networks node mobility can affect the overall performance up to a point where, e.g. route discovery and route establishment fail. As a consequence any formal technique for performance analysis of wireless network protocols should take node mobility into account. In this paper we propose a topology-based mobility model, that abstracts from physical behaviour, and models mobility as probabilistic changes in the topology. We demonstrate how this model can be instantiated to cover the main aspects of the random walk and the random waypoint mobility model. The model is not a stand-alone model, but intended to be used in combination with protocol models. We illustrate this by two application examples: first we show a brief analysis of the Ad-hoc On demand Distance Vector (AODV) routing protocol, and second we combine the mobility model with the Lightweight Medium Access Control (LMAC).
-
Statistical Model Checking of Wireless Mesh Routing Protocols.
University of Augsburg, Germany. July 2013.
abstract | pdf
Abstract:
Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this talk I will illustrate this by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Among others I will show that some optional features of AODV are not useful, and that AODV shows unexpected behaviour-yielding a high chance of route discovery failure.
Last, but not least, I will report on experiments set up in a way to find the benefits and the limits of statistical model checking. In particular I will discuss a result that verifies that this technology is capable of analysing networks of up to 100 nodes.
-
Ad hoc Routing in Mesh Networks using Algebra.
70th meeting of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, Schloss Reisensburg, Germany. July 2013.
abstract | pdf
Abstract:
At the meeting in Rome I gave an overview of formal modelling and analysis of routing protocols for wireless mesh networks (WMNs). Afterwards I was asked to present details about the methods used. This talk presents some more details about the algebra used to model main aspect of routing protocols.
-
Analyse drahtloser Netzwerke mittels Formaler Methoden.
Christian-Abrechts-Universität zu Kiel, Germany. June 2013.
abstract | pdf
Abstract:
Wireless Mesh Netzwerke (WMNe), auch drahtlose, gemaschte Netzwerke genannt, werden heutzutage in einer Vielzahl von Gebieten eingesetzt: Anwendungen reichen von Sicherstellung der öffentlichen Sicherheit, über intelligente Transportsysteme bis hin zu Videoüberwachung. Durch das Fehlen von Kabeln bieten diese Netzwerke eine kostengünstige Alternative zu klassischen Netzwerken und bringen zusätzlich den Vorteil mit sich, dass die Installation einfach und schnell verläuft. Um Daten über solche Netzwerke zu schicken, spielen Routing-Protokolle (Pfadfindung) eine zentrale Rolle; sie müssen insbesondere Besonderheiten von WMNen, wie etwa eine dynamische Topologie oder unzuverlässige Knotenverbindungen berücksichtigen.
Im alltäglichen Einsatz treten massive Probleme in der Performanz und der Zuverlässigkeit dieser Netzwerke auf. Klassische Analysetechniken, wie Simulation und Testbett-Evaluation, konnten diese Probleme bisher nicht lösen, da sie viel Zeit beanspruchen und auch nicht alle Eventualitäten in Betracht ziehen. Eine Folge ist, dass selbst nach Jahren noch Fehler in Routingprotokollen gefunden werden.
Formale Methoden haben das Potenzial, Routing Protokolle präzise zu beschreiben und zu analysieren. In dem Vortrag wird, nach einem kurzen Überblick über WMNe, eines der Standard-Routingprotokolle, das \"Ad-hoc on Demand Distance Vector (AODV) routing protocol\" vorgestellt. Anschliessend wird ein Überblick über formale Methoden präsentiert, die bei NICTA erfolgreich zur Modellierung, Analyse und Verifikation des AODV Protokolls eingesetzt wurden. Behandelt werden ein prozess-algebraischer Ansatz, welcher alle Details von AODV abdeckt, ein Ansatz mittels Linearer Algebra, welcher den Einsatz von automatischen Theorembeweisern ermöglicht, und die Verwendung von Model Checkern.
-
Statistical Model Checking of Wireless Mesh Routing Protocols.
5th NASA Formal Methods Symposium (NFM'13), Mountain View, CA, USA. May 2013.
abstract | pdf
Abstract:
Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this paper we illustrate this by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, we push the limits and show that this technology is capable of analysing networks of up to 100 nodes.
-
Formal Verification of Networks—Description Language—.
NICTA, Sydney, Australia. April 2013.
abstract | pdf
Abstract:
Formal Verification of Networks can only be achieved when the specification (written in English prose) comes along with a formal description of the system. In this talk I will present a description language developed at NICTA to model network protocols for (wireless networks). The language covers main primitives of protocols, such as message passing, and is easy to use.The talk will not only cover details of the language (syntax), but also parts of the underlying semantics. The semantics is given in form of a structural operational semantics which immediately yields an underlying process algebra and allows formal reasoning.
The formal description language builds the base of many useful verification techniques; for example, proof mechanisation using Isabelle/HOL or (statistical) model checking using Uppaal. (these techniques are not part of this talk; but may be part of forthcoming talks)
-
Past and Future of Formal Methods for Wireless Mesh Networks.
Quantitative Methods in Security and Safety Critical Applications, Shonan Village, Japan. November 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by \"hopping\" from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.
The presentation will start with an overview of the (formal) methods for WMNs developed over the last two years. In particular, I will focus on a process-algebraic approach, which turned out to be very useful and powerful, and which can be complemented by model checking. Usability of our approach is illustrated by the analysis of the Ad-hoc On-demand Distance Vector (AODV) routing protocol, a popular routing protocol designed for WMNs, and one of the four protocols currently standardised by the IETF MANET working group.
The talk will then discuss possible directions for future work. In particular, the talk will discuss two topics. (a) the extension of the process-algebraic approach by probabilities to model packet loss and to allow quantitative reasoning (b) the quest of protocol comparison, i.e., under which circumstances is one protocol better than another. Here new formalisms need to be created and evaluated.
-
Towards a Rigorous Analysis of AODVv2 (DYMO).
2nd International Workshop on Rigorous Protocol Engineering, UAustin, TX, USA. October 2012.
abstract | pdf
Abstract:
Dynamic MANET On-demand (AODVv2) routing, formerly known as DYMO, is a routing protocol especially designed for wireless, multi hop networks. AODVv2 determines routes in a network in an on-demand fashion.
In this paper we present a formal model of AODVv2, using the process algebra AWN. The benefit of this is two-fold: (a) the given specification is definitely free of ambiguities; (b) a formal and rigorous analysis of the routing protocol is now feasible. To underpin the latter point we also present a first analysis of the AODVv2 routing protocol. On the one hand we show that some of the problems discovered in the AODV routing protocol, the predecessor of AODVv2, have been addressed and solved. On the other hand we show that other limitations still exist; an example is the establishment of non-optimal routes. Even worse, we locate shortcomings in the AODVv2 routing protocol that do not occur in AODV. This yields the conclusion that AODVv2 is not necessarily better than AODV.
-
A Rigorous Analysis of AODV and its Variants.
15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM'12), Paphos, Cyprus. October 2012.
abstract | pdf
Abstract:
In this talk we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Net- works), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.
-
Kleene Modules for Routing Procedures.
Workshop on Lattices and Relations, Amsterdam, The Netherlands. September 2012.
abstract | pdf
Abstract:
In the past, algebraic techniques based on semirings have been used describe shortest path algorithms and routing procedures. These approaches often use matrices over semirings/Kleene algebra, which form again a semiring/Kleene algebra. While these approaches work well for shortest paths algorithms, they fail when modelling timing aspects of routing algorithms. A major shortcoming is that at least one distributivity law has to be dropped on the level of semiring. This implies the loss of associativity on the matrix-level. In this talk I will present the shortcoming with the help of the Ad hoc On-Demand Distance Vector (AODV) routing protocol. AODV is a widely used and standardised routing protocol designed for wireless mesh networks (WMNs); AODV also forms the basis of new WMN routing protocols, such as the upcoming IEEE 802.11s wireless mesh network standard. I will argue that Kleene modules can help in this regard. I will show how crucial aspects of routing protocols in general, and AODV in particular, can be modelled using modules. The talk will be concluded with some discussion on on-going developments and future work.
-
Towards a Representation Theorem for Coloring Algebra.
Workshop on Lattices and Relations, Amsterdam, The Netherlands. September 2012.
abstract | pdf
Abstract:
Coloring algebra (CA) captures common ideas of feature oriented programming (FOP), a general programming paradigm that provides formalisms, methods, languages, and tools for building main- tainable, customisable, as well as extensible software. FOP has widespread applications from network protocols and data structures to software product lines. It arose from the idea of level-based designs, i.e., the idea that each program (design) can be successively built up by adding more and more levels (features). Later, this idea was generalised to the abstract concept of features. The algebra itself is based on rings and offers simple and concise axioms for feature composition and feature interaction. From these two operations algebraic laws describing products, product lines and other concepts of FOP can be derived. The talk will start with a brief introduction to coloring algebra. In particular I will discuss the interplay between feature composition and interaction. I will also present different models and discuss their relationship to and applicability for feature oriented programming. The examples will show that the choice for defining feature composition is limited. In fact, I will prove that the composition operator is always isomorphic to symmetric-difference in a set-theoretic model. The proof can easily be derived from Kronecker Basis Theorem. By this result we have 'half' a representation theorem for CA. A detailed understanding of feature interaction is missing for the characterisation and the proof of a full representation theorem. Therefore, I will conclude the talk with some observations and conjectures on the structure of coloring algebra, which hopefully helps to come up with a full representation theorem.
-
Morgan: A Suitable Case for Treatment.
Carroll Morgan—Birthday Seminar, University of New South Wales, Sydney, Australia. July 2012.
pdf
Abstract:
-
Formal Methods for Wireless (Mesh) Protocols.
NICTA, Sydney, Australia. April 2012.
pdf
Abstract:
-
A Process Algebra for Wireless Mesh Networks.
21st European Symposium on Programming (ESOP'12), Tallinn, Estonia. March 2012.
abstract | pdf
Abstract:
We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
-
Automated Analysis of AODV using UPPAAL.
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Tallinn, Estonia. March 2012.
abstract | pdf
Abstract:
This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.
We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.
-
Formal Methods for Wireless Mesh Networks.
National University Singapore, Singapore. February 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Formal Methods for Wireless Mesh Networks.
TU München, Germany. February 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work. The latter includes a formal model of process algebra in Isabelle/HOL.
-
Formal Methods for Wireless Mesh Networks.
RWTH Aachen, Germany. February 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Formal Methods for Wireless Mesh Networks.
IFIP WG 2.1, Rome, Italy. February 2012.
pdf
Abstract:
-
Formal Methods for Wireless Mesh Networks.
University of Pisa, Italy. February 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Formal Methods for Wireless Mesh Networks.
University of Bologna, Italy. January 2012.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Formal Methods for Mesh Protocols.
NICTA, Sydney, Australia. January 2012.
pdf
Abstract:
-
Formal Methods for Wireless Mesh Networks.
University of Adelaide, Adelaide, Australia. December 2011.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Modelling and Analysis of AODV in UPPAAL.
1st International Workshop on Rigorous Protocol Engineering, co-located with ICNP 2011, Vancouver, Canada. October 2011.
abstract | pdf
Abstract:
This talk describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks.
We give a brief overview of a model of AODV implemented in the UPPAAL model checker, and describe experiments carried out to explore AODV's behaviour in two network topologies. We were able to locate automatically and confirm some known problematic and undesirable behaviours. We believe this use of model checking as a diagnostic tool complements other formal methods based protocol modelling and verification techniques, such as process algebras. Model checking is in particular useful for the discovery of protocol limitations and in the development of improved variations.
-
A Process Algebra for Wireless Mesh Networks.
University of Augsburg, Augsburg, Germany. June 2011.
abstract | pdf
Abstract:
Wireless Mesh Networks have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment.
Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I propose a process algebra for wireless mesh networks that combines novel treatments of broadcast, prioritised unicast and data structures. In this framework, we modelled the widely-used Ad-hoc On-Demand Distance Vector (AODV) routing protocol and prove crucial properties such as loop freedom.
-
Formal Methods for Wireless Mesh Networks.
University of Augsburg, Augsburg, Germany. June 2011.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment.
Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation.
Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
Towards an Algebra of Routing Tables.
12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS'12), Rotterdam, The Netherlands. June 2011.
abstract | pdf
Abstract:
We use well-known algebraic concepts like semirings and matrices to model and argue about Wireless Mesh Networks. These networks are used in a wide range of application areas, including public safety and transportation. Formal reasoning therefore seems to be necessary to guarantee safety and security. In this paper, we model a simplified algebraic version of the AODV protocol and provide some basic properties. For example we show that each node knows a route to the originator of a message (if there is one).
-
Formal Methods for Wireless Mesh Networks.
University of Cambridge, Cambridge, UK. May 2011.
abstract | pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially self-organising wireless ad-hoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and low-cost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and test-bed experiments. The key limitations of these approaches are that they are very expensive, time consuming and non-exhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"time-to-market\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks. In this talk I describe the importance of WMNs and present one of the leading protocols: the Ad-hoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV . This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.
-
An Algebra for Routing Protocols.
University of Sheffield, Sheffield, UK. May 2011.
pdf
Abstract: