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. She began her career as an assistant professor of computer science at the University of Maryland. From 1981 to 1996 she worked for Bell Laboratories Research, and from 1996 to 2017 she worked for AT&T Labs Research. She is now a research associate in the Department of Computer Science at Princeton University.
Compositional Network Architecture is a comprehensive model of network architecture based on the ideas that a network is a self-contained module, and that network services today are provided by rich, flexible compositions of heterogeneous networks. In these compositions, each network has its own scope of membership, purpose, level of abstraction, and geographical span. Compositional Network Architecture explains how, despite the fact that the IP protocol suite has not changed significantly since 1993, the Internet has evolved to meet many new requirements and challenges since then. The model is precise as well as faithful to the details of real networks, and has been formalized.
Compositional Network Architecture is joint work with Jennifer Rexford. It is the subject of their book The Real Internet Architecture: Past, Present, and Future Evolution (Princeton University Press, August 2024).
An interest in languages for modeling software spans Zave's 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.
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 34 patents in the telecommunications area, and has won two Best Paper awards for telecommunications research. In addition she has been received an AT&T Strategic Patent Award and an AT&T Science and Technology Medal, and was named an AT&T Fellow. In 2017 she received the IEEE Computer Society's Harlan D. Mills Award for "groundbreaking use of formal methods in the development of telecommunication software and for enduring contributions to software engineering theory."
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.
Last updated July 2024.