https://www.dagstuhl.de/10051

January 31 – February 5 , 2010, Dagstuhl Seminar 10051

Quantitative and Qualitative Analysis of Network Protocols

Organizers

Bengt Jonsson (Uppsala University, SE)
Jörg Kreiker (SMA Solar Technology, DE)
Marta Kwiatkowska (University of Oxford, GB)

For support, please contact

Dagstuhl Service Team

Documents

List of Participants
Dagstuhl Seminar Schedule [pdf]

Summary

The Dagstuhl seminar Quantitative and Qualitative Analysis of Network Protocols was held in the week from January 31, 2010 to February 5, 2010. It was the first Dagstuhl seminar to bring together researchers from the network and systems community as well as from the verifi cation community. 10 female and 33 male researchers from institutes in 12 diff erent countries including two industrial participants contributed to the success of this event.

The working hypothesis of this seminar was based on a perceived imbalance. On the one hand network researchers may tend to - in the absence of a suitable modeling discipline - build and then measure rather than to model, verify, and then build. On the other hand, network models analyzed by the formal veri fication community may be overly simpli ed. Below we explain how we went about this imbalance during the seminar.

During the Monday morning session each participant spent a few minutes on her background, her modelling and verifi cation challenges, and her expectations regarding the seminar. In the afternoon four tutorials provided state-of-the-art information representing each of the four communities, where the verifi cation community is viewed as three di erent sub-communities.

On the remaining days we enjoyed 29 talks well distributed over the different communities. Talks addressed plenty of methodologies like simulation, graph theory, graph rewriting, process algebras, static analysis, model checking, quantitative model checking, theorem proving and control theory. All of them were successfully applied to specifi c problems. One of the expected outcomes of the seminar was a benchmark collection. Indeed, a number of the presented case studies may serve this purpose: Chess WSN clock synchronization (Vaandrager), multipath routing (N.Walker), Fraglets, in particular the alternating bit protocol written in Fraglets (Tschudin, Vaandrager), DYMO (Jonsson), AODV (Nanz), ZigBee key establishment (Yuksel), API Authorization (Lee), or Gossip (Bakshi).

Other than the talks we had two long and insightful discussion sessions on Tuesday afternoon and on Friday morning. One key observation from the discussions was that simulations are hard to trust and often do not work. Many people agreed that models cannot be trusted either. On the other hand, it was pointed out that many probabilistic systems tend to behave deterministically in the limit. This allows for continous approximations of discrete behaviour, like the mean field method, the chemical master equation, or statistical model checking. All of these approaches are promising with respect to huge state spaces, which prevent scalability for many discrete, finite abstractions-based methods. A better use of such methods might be the exploration and discovery of corner cases, which can be hard to detect using statistical methods.

We conclude by a few personal remarks. First, it should not go unmentioned, that the seminar su ffered from the unexptected absence of the one organizer representing the network community, Timothy Griffin from Cambridge. It came as a blow to us, just days before the seminar. Second, the seminar took place during a week with heavy snowfall. So much snow, in fact, that virtually all outdoor activities including the traditional Wednesday excursion had to be cancelled. However, ending on a positive note, we were glad to observe a number of inter-community collaborations getting sparked. We are optimistic that these will be perpetuated.

Classification

  • Networks
  • Verification/logic
  • Semantics/formal Methods

Keywords

  • Network protocols
  • Quantitative verification
  • Graph transformation
  • Process calculi

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.