Professional Biography

Education and Employment

Pamela Zave received an A.B. degree in English from Cornell University, and a Ph.D. degree in computer sciences from the University of Wisconsin--Madison. She began her career as an assistant professor of computer science at the University of Maryland--College Park. Since 1981 she has worked for the research organization of AT&T, which was part of Bell Laboratories before 1996 and part of AT&T Laboratories afterward.


Requirements Engineering

In collaboration with Michael Jackson, she put requirements engineering on a firm foundation by defining and elucidating the three major descriptions needed: (1) Domain knowledge (K) describes the domain in which a computer system will be installed. (2) Requirements (R) describe the domain as it ought to be when the computer system is installed and running. (3) Specifications (S) are a subset of requirements; they are requirements confined to the phenomena at the system/domain interface, i.e., phenomena shared by the system and domain. Most importantly, all of these are descriptions of the domain. The proper relationship among the three is given by the formula "S, K |- R", which expresses the obligation that R must be provable from S and K. This formula has been called "the E = mc2 of requirements engineering" by Anthony Hall.

Papers on this work have won Ten-Year Most Influential Paper awards from three different conferences. It is the basis for the REVEAL requirements-engineering method, which is taught and practiced by Praxis in the UK.

Telecommunication Services

Zave was one of the first researchers to recognize that the feature-interaction problem was the greatest challenge of the time in developing telecommunication systems. In 1992 she co-founded a long series of workshops on Feature Interactions in Telecommunications and Software Systems.

Distributed Feature Composition (DFC) is a modular architecture for telecommunication services, designed to provide structured feature composition and easy management of feature interactions. DFC was invented by Zave and Michael Jackson beginning in 1997.

From 1999 to 2012 she worked with a team of AT&T researchers to implement and exploit DFC. This team used DFC to build the advanced features for CallVantage (SM), AT&T's first voice-over-IP service, which became publicly available in 2004 and served approximately 100,000 customers world-wide. Because of DFC, the features were developed with unprecedented speed and quality. CallVantage won two industry awards citing its voice quality and advanced features. After CallVantage this team built, deployed, and maintained the teleconferencing system used internally by AT&T, which supports millions of user minutes each work day. DFC has been incorporated into the Java Community Process standard for SIP Servlet containers. The team also created open-source tools for building SIP-based telecommunication services with DFC principles, and supported AT&T developers who are using these tools.

Zave holds 26 patents in the telecommunications area, and has won two Best Paper awards for telecommunications research.

Modeling and Verification

An interest in languages for modeling software spans her entire career, beginning with invention of the PAISLey executable specification language. Her early papers on executable specifications were widely reprinted and cited (for their time). Early work on multiparadigm specification (composition of specifications in multiple languages) resulted in a Best Paper award from IEEE Software.

More recently, she has carried out significant studies of important protocols.

SIP is the dominant protocol for IP-based multimedia communication, and is the subject of many thousands of pages in hundreds of IETF standards documents. Her Promela models of SIP, analyzed with the model-checker Spin, are the first formal models of this important application protocol. She used them to discover and explain many previously unknown inconsistencies, ambiguities, and race conditions.

The distributed hash table Chord was presented in a SIGCOMM paper that was the fourth-most-cited paper in computer science for several years (according to Citeseer), and won the 2011 SIGCOMM Test-of-Time Award. The introduction says, ``Three features that distinguish Chord from many other peer-to-peer lookup protocols are its simplicity, provable correctness, and provable performance.'' Yet she showed using Alloy that the protocol is not correct, and that not one of the seven properties claimed to be invariants is actually an invariant. Since then she has developed a correct and easily implementable version of Chord, along with an inductive invariant and a proof of correctness. Engineers at Amazon have credited this work with convincing them to start using formal methods to find bugs in Amazon's distributed systems.

Patterns in Network Architecture

She is currently interested in abstractions of network architectures that will make it possible to compare, compose, and re-use solutions to individual networking problems. Such abstractions would help the Internet evolve to meet present and future requirements that are ill-satisfied today. They would also help software engineers contribute to Internet architecture, and improve the Internet as a platform for building and deploying innovative applications.

Working with Jennifer Rexford of Princeton University, she has proposed a "geomorphic view" of networking as the fundamental abstraction. The geomorphic view has been used to organize and survey the design space of network mobility in their chapter of the textbook Recent Advances in Networking, published electronically by ACM SIGCOMM. This abstraction has also led to the discovery that there are two fundamental patterns for implementing mobility, and a proof that the patterns are compositional.

In current work, Zave and Rexford are exploring applications of the geomorphic view to middleboxes, security, and teaching networking.


Service (Selected)

Invited Talks (Selected)

Last updated July 2015.