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.
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.
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 31 patents in the telecommunications area, and has won two Best Paper awards for telecommunications research.
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.
Compositional Network Architecture is a comprehensive model of networking 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. Networks are composed by bridging, with the obvious meaning, and layering, which means something new and very precise. 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 and formalized this compositional architecture. The new model has proven very fruitful for discovering patterns and principles in the design of networks. They are working on a networking textbook from this perspective. They are also engaged in a research project to embody the model in an implementation in P4, so they can explore model-driven design, development, and verification of networks. The biggest benefit of the model for network practitioners is that it explains layering in a new way that is realistic, precise, and offers strong modularity to exploit for reuse and verification.
Last updated June 2020.