Correctness is important in data-plane programs, which run on critical infrastructure connecting millions of users. Verification helps programmers build correct software, but current data-plane tools can only check simple properties or require immense programmer effort. As a solution, this paper introduces the first verification-aware data-plane language: VeriLucid. The core idea is to unify programming and specification in one high-level language, with built-in proof automation. Integration makes it natural for programmers to use verification continuously throughout development, like unit testing but with strong guarantees. In evaluation, we show that VeriLucid requires 10X less programmer effort, in terms of lines of code, than other verification tools with comparable expressiveness.

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 prototype, we show that Dysco is provably correct, highly scalable, and able to reconfigure service chains across a range of middleboxes.

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.

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.

Abstract 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.

Model Management addresses the problem of managing an evolving collection of models by capturing the relationships between models and providing well-defined operators to manipulate them. In this paper, we describe two such operators for manipulating feature specifications described using hierarchical state machine models: Match, for finding correspondences between models, and Merge, for combining models with respect to known or hypothesized correspondences between them. Our Match operator is heuristic, making use of both static and behavioral properties of the models to improve the accuracy of matching. Our Merge operator preserves the hierarchical structure of the input models, and handles differences in behavior through parameterization. This enables us to automatically construct merges that preserve the semantics of hierarchical state machines. We report on tool support for our Match and Merge operators, and illustrate and evaluate our work by applying these operators to a set of telecommunication features built by AT&T.

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.

Synthesis of system configurations from a given set of features is an important and very challenging problem. This paper makes a step towards this goal by describing an efficient technique for synthesizing pipeline configurations of feature-based systems. We identify and formalize a design pattern that is commonly used in featurebased development. We show that this pattern enables compositional synthesis of feature arrangements. In particular, the pattern allows us to add or remove features from an existing system without having to reconfigure the system from scratch. We describe an implementation of our technique and evaluate its applicability and effectiveness using a set of telecommunication features from AT&T, arranged within the DFC architecture.

Model Management addresses the problem of managing an evolving collection of models, by capturing the relationships between models and providing well-defined operators to manipulate them. In this paper, we describe two such operators for manipulating hierarchical Statecharts: Match, for finding correspondences between models, and Merge, for combining models with respect to known correspondences between them. Our Match operator is heuristic, making use of both static and behavioural properties of the models to improve the accuracy of matching. Our Merge operator preserves the hierarchical structure of the input models, and handles differences in behaviour through parameterization. In this way, we automatically construct merges that preserve the semantics of Statecharts models. We illustrate and evaluate our work by applying our operators to AT&T telecommunication features.

When there is more than one application server in the signaling path between IP media endpoints, and the servers manipulate media flow, media flow must be controlled com-positionally. This paper presents a protocol, signaling architecture, API, and API implementation for distributed, compositional media control. The semantics of the API is specified in linear temporal logic, and the implementation has been partially verified by model checking. The principles developed to solve this problem may be useful for making other network applications compositional.

Ten years ago, our paper described how a very small system might be developed to control a coin-operated turnstile in a zoo [1]. It arose out of our efforts to understand how requirements, domain knowledge and specifications fit together, and how specifications could be derived systematically. A particular goal was to understand requirements and specifications for telecommunication systems well enough to handle the feature interaction problem that plagues telecommunication software.A year later we published a more comprehensive version of our requirements framework [3], and began to develop the Distributed Feature Composition (DFC) architecture for telecommunication services [2]. We continued to work on it together until mid-2002. DFC has proven successful in practice, and is now being used in a commercial voice-over-IP service.Since publishing the requirements framework, we have worked on different kinds of system, and have been confronted with important differences in how its principles apply. It has taken all this time to achieve the goal of understanding requirements for telecommunication services and other connection services. In this domain, requirements are heavily influenced by the fact that services are assemblies of components added to a basic network infrastructure. Our work in another direction has led to a focus on system interaction with the human and physical world, recognising the varying roles of formalisation and formal reasoning in problems of different kinds, and the need for a stronger grip on the relationship between engineering of software and engineering in the world.The common lesson of these experiences is that the requirements framework of ten years ago is a good generalization, but specific domains and situations require their own specializations of it.

An open (in the sense of extensible and programmable) architecture for IP telecommunications must be based on a comprehensive strategy for managing feature interaction. We describe our experience with BoxOS, an IP telecommunication platform that implements the DFC technology for feature composition. We present solutions to problems, common to all efforts in IP telecommunications, of feature distribution, interoperability, and media management. We also explain how BoxOS addresses many deficiencies in SIP, including how BoxOS can be used as a SIP application server.

Address translation causes a wide variety of interactions among telecommunication features. This article begins with a formal model of address translation and its effects, and with principles for understanding how features should interact in the presence of address translation. There is a simple and intuitive set of constraints on feature behavior so that features will interact according to the principles. This scheme (called "ideal address translation") has provable properties, is modular (explicit cooperation among features is not required), and supports extensibility (adding new features does not require changing old features). The article also covers reasoning in the presence of exceptions to the constraints, limitations of the theory, relation to real networks and protocols, and relation to other research.

Previous work in distributed feature composition architecture has shown that a modular, compositional architecture of feature logic can lead to successful management of feature interaction. It can also promote rapid deployment of new services and third party innovation in a communication network. ECLIPSE is an implementation of DFC that focuses on voice over IP (VoIP) and multimedia over IP. In ECLIPSE, the signaling messages traverse units of feature logic (feature boxes), but by necessity the media data have to take a separate and more direct path. This paper describes a scheme in which the feature boxes can cooperatively control the flow of media in an optimal path, while still maintaining the benefits of the DFC architecture. This scheme supports any desired media connectivity, and is independent of VoIP protocols (e.g. SIP and H.323), or the underlying media switch fabric implementation. This result is also applicable to other component architectures for communications. Comparison is made with other schemes proposed in the literature.

In many software application domains, constant evolution is the dominant problem, shaping both software design and the software process. Telecommunication software is the prototypical example of such an application domain. This paper examines how requirements engineering, formal description techniques and formal methods should be adapted to work well in these application domains.

Distributed Feature Composition (DFC) is a new technology for feature specification and composition, based on a virtual architecture offering benefits analogous to those of a pipe-and-filter architecture. In the DFC architecture, customer calls are processed by dynamically assembled configurations of filter-like components: each component implements an applicable feature, and communicates with its neighbors by featureless internal calls that are connected by the underlying architectural substrate.

In engineering the requirements for a telecommunications system, the greatest obstacle to be overcome is the sheer complexity of the required behavior. We present several ways of managing and minimizing this complexity, all of proven effectiveness. Most of the specification techniques result from specific application of general requirements principles to the telecommunications domain.

Research in requirements engineering has produced an extensive body of knowledge, but there are four areas in which the foundation of the discipline seems weak or obscure. This article shines some light in the “four dark corners,” exposing problems and proposing solutions. We show that all descriptions involved in requirements engineering should be descriptions of the environment. We show that certain control information is necessary for sound requirements engineering, and we explain the close association between domain knowledge and refinement of requirements. Together these conclusions explain the precise nature of requirements, specifications, and domain knowledge, as well as the precise nature of the relationships among them. They establish minimum standards for what information should be represented in a requirements language. They also make it possible to determine exactly what it means for requirements and engineering to be successfully completed.

Proposes a technique to help people organize and write complex specifications, exploiting the best features of several different specification languages. Z is supplemented, primarily with automata and grammars, to provide a rigorous and systematic mapping from input stimuli to convenient operations and arguments for the Z specification. Consistency analysis of the resulting specification is based on the structural rules. The technique is illustrated by two examples, a graphical human-computer interface and a telecommunications system.

A requirement is a desired relationship among phenomena of the environment of a system, to be brought about by the hardware/software machine that will be constructed and installed in the environment.A specification describes machine behaviour sufficient to achieve the requirement.A specification is a restricted kind of requirement all the environment phenomena mentioned in a specitlcation are shared with the machinq the phenomena constrained by the speciilcation are controlled by the machine; and the specified constraints can be determined without reference to the future.Specflcations are derived from requirements by reasoning about the environtnen~using properties that hold independently of the behaviour of the machine.These ideas, and some associated techniques of description, are illustrated by a simple example.

The article proposes and justifies a trial classification scheme. An earlier version was used to organize the papers submitted to this symposium, and the scheme has been refined somewhat in response to inadequacies discovered during the process of selecting the program. The first issue to be tackled is the heterogeneity of the topics usually considered part of requirements engineering. They include: tasks that must be completed; problems that must be solved; solutions to problems; ways of contributing to knowledge; and types of system. There seems to be a need for several orthogonal dimensions of classification. While multiple dimensions certainly help us cope with the heterogeneity of concerns, there is a danger of making the classification scheme too complex to use. I have compromised by settling on two dimensions.

Ideas about the meaning of descriptions, aimed at clarifying the relationship between a formal specification and the domain of the system to be specified, are introduced. Understanding of specifications must rest on explicit statements of what they are about and what they assert. The authors argue that current formal specification techniques are inadequate in this respect, and therefore cannot offer a satisfactory foundation for automated support of software development. An approach that offers a possible basis for effective reuse of descriptions generally, and of partial specifications in particular, is discussed.>

Partial specifications written in many different specification languages can be composed if they are all given semantics in the same domain, or alternatively, all translated into a common style of predicate logic. The common semantic domain must be very general, the particular semantics assigned to each specification language must be conducive to composition, and there must be some means of communication that enables specifications to build on one another. The criteria for success are that a wide variety of specification languages should be accommodated, there should be no restrictions on where boundaries between languages can be placed, and intuitive expectations of the specifier should be met.

An executable specification language called PAISLey is evaluated. The language is accompanied by specification methods, analysis techniques, and software tools. The actual results of the PAISLey project are summarized. Research methods, how the results were obtained, and how the project might have been improved are discussed.>

It is shown that a multilanguage approach can provide more useful feedback than the use of any single specification language by itself. The point is illustrated by an architectural model written in two executable specification languages, PAISLey and CSP. The model can be subjected to formal type checking, protocol analysis and timing analysis. In all three cases, a notion of consistency between developmental stages of the model is enforced.>

We describe why these papers were chosen, and categorize them in terms of major contribution, underlying model of the software life-cycle, and applicability to various types of system.

The executable specification language PAISLey and its environment are presented as a case study in the design of computer languages. It is shown that PAISLey is unusual (and for some features unique) in having the following desirable features: (1) there is both synchronous and asynchronous parallelism free of mutual-exclusion problems, (2) all computations are encapsulated, (3) specifications in the language can be executed no matter how incomplete they are, (4) timing constraints are executable, (5) specifications are organized so that bounded resource consumption can be guaranteed, (6) almost all forms of inconsistency can be detected by automated checking, and (7) a notable degree of simplicity is maintained. Conclusions are drawn concerning the differences between executable specification languages and programming languages, and potential uses for PAISLey are given.

A specification technique, formally equivalent to finite-state machines, is offered as an alternative because it is inherently distributed and more comprehensible. When applied to modules whose complexity is dominated by control, the technique guides the analyst to an effective decomposition of complexity, encourages well-structured error handling, and offers an opportunity for parallel computation. When applied to distributed protocols, the technique provides a unique perspective and facilitates automatic detection of some classes of error. These applications are illustrated by a controller for a distributed telephone system and the full-duplex alternating-bit protocol for data communication. Several schemes are presented for executing the resulting specifications.

An experimental implementation of a design for an adaptive, parallel finite-element system is described.The implementation was used to simulate the performance of this design on several microprocessor-based multiprocessor architectures The real-time speedup observed was architectureindependent, but hmited.Nevertheless, the approach to data segmentation and management worked well and has interesting applications.

Complex systems (such as distributed ones) should be specified before they are implemented. Even more advantages accrue if the specifications are executable, so that behaviors of the specified systems can be tested. This paper addresses practical questions such as how incomplete specifications can be tested, and what kind of interface is needed to control tests of distributed systems. The answers take the form of a concrete proposal which has been implemented in prototype form.

The approach to requirements specification for embedded systems described in this paper is called "operational" because a requirements specification is an executable model of the proposed system interacting with its environment. The approach is embodied by the language PAISLey, which is motivated and defined herein. Embedded systems are characterized by asynchronous parallelism, even at the requirements level; PAISLey specifications are constructed by interacting processes so that this can be represented directly. Embedded systems are also characterized by urgent performance requirements, and PAISLey offers a formal, but intuitive, treatment of performance.

This paper argues that system requirements should be specified in terms of an interpretable model, including non-logical (performance and resource) properties, of the system interacting with its environment. The specification language should be integrated with a methodology capable of using hierarchies and projections to decompose complexity, and covering analysis and design as well as requirements specification. A language embodying these ideas is described, and early experience with it is reported.

A design for a novel prototype finite element system is presented which meets the following four goals: the system constitutes an application-independent finite element solver for a certain class of linear elliptic problems based on a weak mathematical formulation; it incorporates extensive adaptive approaches to minimize the critical decisions demanded of the user; it incorporates adaptive error estimation techniques to provide an optimal solution within a prescribed cost range; and it takes advantage of natural parallelism and modularity to increase the size of the practically solvable problems. The overall system structure is described in terms of parallel processes and is implementable on a wide variety of hardware configurations. The experiments planned to evaluate the various new approaches are also presented. (Author)