Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 10051

Quantitative and Qualitative Analysis of Network Protocols

( Jan 31 – Feb 05, 2010 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:




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 verification community. 10 female and 33 male researchers from institutes in 12 different 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 verification community may be overly simplified. 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 verification 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 verification community is viewed as three different 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 specific 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 continuous approximations of discrete behavior, 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 suffered 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.

  • Miguel Andres (Radboud University Nijmegen, NL)
  • Christel Baier (TU Dresden, DE) [dblp]
  • Rena Bakhshi (Free University of Amsterdam, NL)
  • Paolo Baldan (University of Padova, IT) [dblp]
  • Doina Bucur (INCAS3, NL)
  • Ana Rosa Cavalli (Télécom & Management SudParis - Evry, FR)
  • Pietro Cenciarelli (Sapienza University of Rome, IT)
  • Pedro R. D'Argenio (Universidad Nacional de Córdoba, AR)
  • Pieter-Tjerk de Boer (University of Twente, NL) [dblp]
  • Javier Esparza (TU München, DE) [dblp]
  • Han Gao (Technical University of Denmark - Lyngby, DK)
  • Kanchi Gopinath (Indian Institute of Science, IN)
  • Daniele Gorla (Sapienza University of Rome, IT)
  • Boudewijn Haverkort (University of Twente, NL) [dblp]
  • Holger Hermanns (Universität des Saarlandes, DE) [dblp]
  • Bengt Jonsson (Uppsala University, SE) [dblp]
  • Joost-Pieter Katoen (RWTH Aachen, DE) [dblp]
  • Barbara König (Universität Duisburg-Essen, DE) [dblp]
  • Jörg Kreiker (SMA Solar Technology, DE)
  • Marta Kwiatkowska (University of Oxford, GB) [dblp]
  • David B. Lee (Ohio State University - Columbus, US)
  • Axel Legay (University of Liège, BE) [dblp]
  • Annabelle McIver (Macquarie University - Sydney, AU) [dblp]
  • Roland Meyer (TU Kaiserslautern, DE) [dblp]
  • Thomas Meyer (Universität Basel, CH)
  • Mirco Musolesi (University of Birmingham, GB)
  • Sebastian Nanz (ETH Zürich, CH)
  • Bo Friis Nielsen (Technical University of Denmark - Lyngby, DK)
  • Flemming Nielson (Technical University of Denmark - Lyngby, DK) [dblp]
  • Catuscia Palamidessi (Ecole Polytechnique - Palaiseau, FR) [dblp]
  • David Parker (University of Oxford, GB) [dblp]
  • Dimosthenis Pediaditakis (Imperial College London, GB)
  • Hanne Riis Nielson (Technical University of Denmark - Lyngby, DK) [dblp]
  • Jeremy Sproston (University of Turin, IT) [dblp]
  • Tobe Toben (OFFIS - Oldenburg, DE)
  • Christian Tschudin (Universität Basel, CH) [dblp]
  • Frits Vaandrager (Radboud University Nijmegen, NL) [dblp]
  • Jaco van de Pol (University of Twente, NL) [dblp]
  • Nigel Walker (British Telecom R&D - Ipswich, GB)
  • Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
  • Bernd Westphal (Universität Freiburg, DE)
  • Peng Wu (University College London, GB)
  • Ender Yüksel (Technical University of Denmark - Lyngby, DK)

  • networks
  • verification/logic
  • semantics/formal methods

  • network protocols
  • quantitative verification
  • graph transformation
  • process calculi