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 firmer foundation by elucidating how and why requirements (R) are statements about the environment or domain of a computer system, and not about the system itself. Domain knowledge (K) consists of intrinsic properties of the domain. Specifications (S) are requirements on the interface, which belongs to both the system and its environment. This work can be summarized 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

She was a founder of a long series of workshops on Feature Interactions in Telecommunications and Software Systems; they began in 1992 as a response to the greatest challenge of the time in developing telecommunication 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 defined by Zave and Michael Jackson beginning in 1997.

Since 1999 she has 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. Since then this team has 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 continues to work on open-source tools for building SIP-based telecommunication services with DFC principles, and on supporting AT&T developers who are using these tools.

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

Internet Architecture

She is currently interested in abstractions for 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, to be 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.

Modeling Languages

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.

Most recently she has been working on applications and comparisons of Alloy and Promela, which are very different languages for lightweight modeling and analysis of software systems. Her Promela models of SIP, analyzed with the model-checker Spin, are the first formal models of this important application protocol. Her Alloy models of Chord, analyzed with the Alloy model-enumeration tool, have revealed that this important protocol is not correct. They have also led to the first provably-correct version.


Service (Selected)

Invited Talks (Selected)

Last updated March 2013.