Composable Asynchronous Events/Formal Methods for Wireless Mesh Networks

Add to your list(s) Download to your calendar using vCal

• Suresh Jagannathan/Peter Höfner
• Monday 23 May 2011, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Peter Sewell.

Note unusual start time: talks at 12.50 prompt

Composable Asynchronous Events

Suresh Jagannathan Purdue University

Although asynchronous communication is an important feature of many concurrent systems, building composable abstractions that leverage asynchrony is challenging. This is because an asynchronous operation necessarily involves two distinct threads of control—the thread that initiates the operation, and the thread that discharges it.

In this talk, we present the design and rationale for asynchronous events, an abstraction that enables composable construction of complex asynchronous protocols, which leverages Concurrent ML’s first-class event structure. We discuss the definition of a number of useful asynchronous abstractions that can be built on top of asynchronous events (e.g., composable callbacks) and provide details of a case study that show how they can be used to improve the modularity and performance of a highly-concurrent server application.

=====================================================================

Formal Methods for Wireless Mesh Networks Peter Höfner

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.

Bio === Peter Höfner is a researcher at National ICT Australia (NICTA) and conjoint lecturer at the School of Computer Science and Engineering at the University of New South Wales, Sydney, Australia. His research interests are focused on applications of formal methods in informatics, including software engineering, hybrid systems, and protocol verification. He holds a diploma degree in mathematics from the the University of Augsburg and received his PhD at the same institute at 2009.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.