Internet of Things (IoT) frequently involves conflicting interactions between devices and features that must be resolved to a single system state. The problem of feature interaction (FI) resolution has been investigated in Software Engineering through approaches that focus on verifiability but usually do not include the user in the evaluation. This paper bridges the gap between IoT approaches in HCI and Software Engineering by applying qualitative methods to understanding users' mental models of one representative FI resolution mechanism. Our contributions are in identifying common mental model errors and biases and how these may inform future IoT systems and research.

The Chord distributed hash table (DHT) is well-known and often used to implement peer-to-peer systems. Chord peers find other peers, and access their data, through a ring-shaped pointer structure in a large identifier space. Despite claims of proven correctness, i.e., eventual reachability, previous work has shown that the Chord ring-maintenance protocol is not correct under its original operating assumptions. Previous work has not, however, discovered whether Chord could be made correct under the same assumptions. The contribution of this paper is to provide the first specification of correct operations and initialization for Chord, an inductive invariant that is necessary and sufficient to support a proof of correctness, and two independent proofs of correctness. One proof is informal and intuitive, and applies to networks of any size. The other proof is based on a formal model in Alloy, and uses fully automated analysis to prove the assertions for networks of bounded size. The two proofs complement each other in several important ways.

Internet of Things (IoT) frequently involves conflicting interactions between devices and features that must be resolved to a single system state. The problem of feature interaction (FI) resolution has been investigated in Software Engineering through approaches that focus on verifiability but usually do not include the user in the evaluation. This paper bridges the gap between IoT approaches in HCI and Software Engineering by applying qualitative methods to understanding users' mental models of one representative FI resolution mechanism. Our contributions are in identifying common mental model errors and biases and how these may inform future IoT systems and research.

Middleboxes are crucial for improving network security and performance, but only if the right traffic goes through the right middleboxes at the right time. Existing traffic-steering techniques rely on a central controller to install fine-grained forwarding rules in network elements---at the expense of a large number of rules, a central point of failure, challenges in ensuring all packets of a session traverse the same middleboxes, and difficulties with middleboxes that modify the "five tuple." We argue that a session-level protocol is a fundamentally better approach to traffic steering, while naturally supporting host mobility and multihoming in an integrated fashion. In addition, a session-level protocol can enable new capabilities like dynamic service chaining, where the sequence of middleboxes can change during the life of a session, e.g., to remove a load-balancer that is no longer needed, replace a middlebox undergoing maintenance, or add a packet scrubber when traffic looks suspicious. Our Dysco protocol steers the packets of a TCP session through a service chain, and can dynamically reconfigure the chain for an ongoing session. Dysco requires no changes to end-host and middlebox applications, host TCP stacks, or IP routing. Dysco's distributed reconfiguration protocol handles the removal of proxies that terminate TCP connections, middleboxes that change the size of a byte stream, and concurrent requests to reconfigure different parts of a chain. Through formal verification using Spin and experiments with our Linux-based prototype, we show that Dysco is provably correct, highly scalable, and able to reconfigure service chains across a range of middleboxes.

In 2025 semantic tools for software engineering will be mature, and their frequency of use in software development will still be disappointing. This proposal explains how research directed at building theories of everything (or, at least, important software domains) can consolidate progress and bring semantic tools into the mainstream of software practice.

Because potential users have to choose a formal method before they can start using one, research on assessing the applicability of specific formal methods might be as effective in encouraging their use as work on the methods themselves. This comparison of Alloy and Spin is based on a demanding project that exploited the full capabilities of both languages and tools. The study exposed issues not apparent from more superficial studies, and resulted in some unexpected conclusions. The paper provides tentative recommendations for two different classes of network protocol, a research agenda for solidifying the recommendations, and a few general lessons learned about research on selection of formal methods.

While the Internet is increasingly mobile, seamless mobility is difficult to implement at Internet scale. Over the years, standards bodies and the research community have introduced a large and confusing collection of mobility proposals that are difficult to compare. In this tutorial, we present these mobility proposals in a uniform framework, called the geomorphic view of networking. The geomorphic view shows that there are two distinct patterns for implementing mobility, each with its own range of design choices and cost-benefit trade-offs. We use these patterns to classify and explain a representative sample of mobility mechanisms, abstractly yet precisely. The patterns also serve as a basis for evaluating properties of these mechanisms such as resource costs and scalability, and for considering composition of mobility mechanisms.

Correctness of the Chord ring-maintenance protocol would mean that the protocol can eventually repair all disruptions in the ring structure, given ample time and no further disruptions while it is working. In other words, it is "eventual reachability." Under the same assumptions about failure behavior as made in the Chord papers, no published version of Chord is correct. This result is based on modeling the protocol in Alloy and analyzing it with the Alloy Analyzer. By combining the right selection of pseudocode and textual hints from several papers, and fixing flaws revealed by analysis, it is possible to get a version that may be correct. The paper also discusses the significance of these results, describes briefly how Alloy is used to model and reason about Chord, and compares Alloy analysis to model-checking.

StratoSIP (“SIP at a very high level”) is a domainspecific language for programming SIP applications. This manual documents Version 1.0 of StratoSIP. The runtime environment for a StratoSIP program is a SIP Servlet container [6]. StratoSIP is compiled into ECharts for SIP Servlets (E4SS) [3]; E4SS is, in turn, compiled into Java. StratoSIP is designed to enable all application programmers, even those with minimal knowledge of SIP, to program SIP applications easily and correctly. At the same time, it provides SIP experts with sufficient control over the detailed signaling behavior of their programs. This manual is also designed to serve both audiences. Its main text is intended for ordinary application programmers. For SIP experts, there is supplementary information in two places. Any section may have a supplementary part at the end labeled “For SIP experts”. In addition, footnotes clarify statements in the main text that might seem oversimplified and therefore confusing to a SIP expert.

Voice-over-IP holds the promise of opening up the telecom domain to a vast community of developers. However, due to the nature of real-time multi-party communication and the complexity of the protocol, writing SIP applications that operate correctly and robustly is very challenging and requires in-depth knowledge. Even with standardized programming paradigms such as the Java-based SIP Servlet API, SIP application programming remains difficult.

This paper presents three conclusions about the description of protocols, based on extensive experience: (1) Informal methods are inadequate for widely used protocols. (2) Lightweight formal methods are easy and useful. (3) Informal natural language cannot be trusted, but natural-language paraphrases of formal language can be trusted for certain purposes. None of these conclusions will be new or surprising to participants in this workshop. The purpose of this paper is to provide new, specific, and relevant evidence for these conclusions, in the hopes that researchers can use this evidence to justify their methods and influence the thinking of others.

The Internet has changed the world. Its astounding success has led to explosive growth in users, traffic, and applications, which has made its original architecture and protocols obsolete. Currently the networking community is questioning all aspects of Internet technology, as researchers and stakeholders try to understand how to meet new requirements for functionality, quality of service, availability, and security. In this technological crisis, one of our most powerful technical tools, namely functional modeling (as opposed to performance modeling), is being completely ignored. In this talk I explain how modeling can be put to good use in the Internet context, how the culture of the Internet Engineering Task Force and the networking research community resist such efforts, and what might be done to bring about a cultural change. The talk will be illustrated with examples and results from several projects using different modeling languages and techniques. These include: The descriptions of these projects will emphasize topics such as the search for the right modeling language and the search for principles of networking.

In SIP services, back-to-back user agents (B2BUAs) are powerful but difficult to program correctly. StratoSIP is a high-level, domain-specific language for programming SIP B2BUAs safely. This paper describes the four major abstractions on which the language is based. It explains how each abstraction is used in programming, and how it is implemented in SIP. Because the abstractions are derived from the Distributed Feature Composition (DFC) architecture, Strato-SIP programs compose easily with each other at runtime. The implementation of StratoSIP runs in SIP Servlet containers.

In many IP media services, the media channels are point-to-point, dynamic, and set up with the participation of one or more application servers, even thou the media packets themselves travel directly between media endpoints. The application servers must be programmed so that media behavior is globally correct, even though the servers may attempt to manipulate the same media channels concurrently and without knowledge of each other. Our proposed solution to this problem of compositional media control includes an architecture-independent descriptive model, a set of high-level programming primitives, a formal specification of their compositional semantics, a signaling protocol, an implementation, and partial verification of correctness. The paper includes performance analysis, comparison to related work, and principles for making other networked applications more compositional.