BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Composable Asynchronous Events/Formal Methods for Wireless Mesh Ne
 tworks - Suresh  Jagannathan/Peter Höfner
DTSTART:20110523T114500Z
DTEND:20110523T130000Z
UID:TALK31526@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Composable Asynchronous Events\n\nSuresh Jagannathan\nPurdue U
 niversity\n\nAlthough asynchronous communication is an important feature o
 f many\nconcurrent systems\, building composable abstractions that leverag
 e\nasynchrony is challenging.  This is because an asynchronous operation\n
 necessarily involves two distinct threads of control -- the thread\nthat i
 nitiates the operation\, and the thread that discharges it.\n\nIn this tal
 k\, we present the design and rationale for asynchronous\nevents\, an abst
 raction that enables composable construction of complex\nasynchronous prot
 ocols\, which leverages Concurrent ML's first-class event\nstructure.  We 
 discuss the definition of a number of useful\nasynchronous abstractions th
 at can be built on top of asynchronous\nevents (e.g.\, composable callback
 s) and provide details of a case\nstudy that show how they can be used to 
 improve the modularity and\nperformance of a highly-concurrent server appl
 ication.\n\n\n\n==========================================================
 ===========\n\n\nFormal Methods for Wireless Mesh Networks     Peter Höfn
 er\n\nWireless Mesh Networks (WMNs) have recently gained considerable\npop
 ularity and are increasingly deployed in a wide range of\napplication scen
 arios\, including emergency response communication\,\nintelligent transpor
 tation systems\, mining\, video surveillance\, etc.\nWMNs are essentially 
 self-organising wireless ad-hoc networks that can\nprovide broadband commu
 nication without relying on a wired backhaul\ninfrastructure.  This has th
 e benefit of rapid and low-cost network\ndeployment.  Traditionally\, the 
 main tools for evaluating and\nvalidating network protocol are simulation 
 and test-bed experiments.\nThe key limitations of these approaches are tha
 t they are very\nexpensive\, time consuming and non-exhaustive. As a resul
 t\, protocol\nerrors and limitations are still found many years after the 
 definition\nand standardisation.  Formal methods have a great potential in
  helping\nto address this problem\, and can provide valuable tools for the
 \ndesign\, evaluation and verification of WMN routing protocols. The\nover
 all goal is to reduce the ``time-to-market'' for better (new or\nmodified)
  WMN protocols\, and to increase the reliability and\nperformance of the c
 orresponding networks.  In this talk I describe\nthe importance of WMNs an
 d present one of the leading protocols: the\nAd-hoc on Demand Distance Vec
 tor (AODV) routing protocol.  Moreover\, I\ngive an overview over formal m
 ethods used so far to model\, analyse and\nverify AODV.  This includes a f
 ormal model using process algebra\,\nfully automation by a matrix model an
 d the use of model checkers. In\nan outlook I present some problems we are
  faced and discuss ongoing\nand future work.\n\n\nBio\n===\nPeter Höfner 
 is a researcher at National ICT Australia (NICTA)\nand conjoint lecturer a
 t the School of Computer Science and\nEngineering at the University of New
  South Wales\, Sydney\,\nAustralia. His research interests are focused on 
 applications\nof formal methods in informatics\, including software engine
 ering\,\nhybrid systems\, and protocol verification.\nHe holds a diploma d
 egree in mathematics from the\nthe University of Augsburg and received his
  PhD at\nthe same institute at 2009.\n\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR