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. From 1981 to 1996 she worked for Bell Laboratories Research (then a part of AT&T), and from 1996 to 2017 she worked for AT&T Laboratories Research. She is now a research associate in the Department of Computer Science at Princeton University.



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 29 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. Leslie Lamport, in his 2014 Turing Lecture, told researchers that awareness of this work is what they need to guide their efforts in the next 25 years.

The Compositional Architecture of the Internet

Contrary to the "classic" Internet architecture familiar to most people, today's Internet is a composition of a wide variety of networks. The IP protocol suite offers a general-purpose network design with a widely available implementation; as such, it is re-used to design and implement networks with many different purposes, with many different scopes, and at different levels of abstraction. Compositional architecture explains how, despite the fact that IP has not changed significantly since 1993, the Internet has evolved to meet many new requirements and challenges since then.

Working with Jennifer Rexford of Princeton University, Zave has explained this compositional architecture. They have argued that understanding and modeling network composition is the key to continued evolution of the Internet, and to meeting society's demands for Internet services that can be verified to meet their requirements, particularly for security and reliability. They have used this view 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.

In 2017 Zave taught a graduate course at Princeton University on Patterns in Network Architecture. She is continuing to work on formal modeling of network architecture and its implications for network design, verification, and evolution.

Service (Selected)

Invited Talks (Selected)

Last updated November 2017.