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.