Pamela Zave's Research Home Page

After many happy years at Bell Laboratories Research and AT&T Laboratories Research, I am now a research associate in the Department of Computer Science at Princeton University.

Permanent Contact Information:

pamela AT pamelazave DOT com

pamelazave AT gmail DOT com

NOW AVAILABLE!

30% Off with Code P327 on orders from Princeton University Press

This book meets a long-standing need for an explanation of how the Internet's architecture has evolved since its creation to perform an ever-broader range of the world's communication tasks. The book introduces a new model of network architecture, called Compositional Network Architecture, that exploits a powerful form of modularity to provide lucid, insightful descriptions of complex structures, functions, and behaviors in today's Internet. Because of the model's generality, the original Internet architecture, today's Internet architecture, and many possible future Internets are all instances of it.

For practitioners, the book offers a precise and realistic approach to comparing design alternatives and guiding the ongoing evolution of their applications, technologies, and security practices.

For educators and students, the book provides patterns that recur in many variations, in many places in the Internet ecosystem. Each pattern tells a compelling story with a common problem to be solved and a range of solutions for solving it, which conveys engineering knowledge and and helps to present the ever-growing set of networking topics in a concise and intuitive manner.

For researchers, the existence of a rigorous formal model of network architecture opens new possibilities for network analysis and development, based on modular reasoning, code synthesis, and verification of user-level service properties.

Also check Compositional Network Architecture for book-related resources.

Professional Biography

Research Interests (Papers and Talks Included)

NEW! Validation of formal models: A case study

Looking for a great classroom example of the use of Alloy? "Validation of formal models: A case study" (Pamela Zave and Tim Nelson) is based on a short course we taught at the 12th Summer School on Formal Techniques in 2023. Our zip file of Alloy models contains a series of Alloy models of the well-known Peterson lock for multiprocessor programming, improving gradually as the locking algorithm gets better and the formal model is validated. The paper documents the progression of Alloy models.

Networking

Software Modeling and Verification

Telecommunication Services

Publications (Selected)

Now available: Software Requirements and Design: The Work of Michael Jackson.

This book spans the career of one of software engineering's most important figures. Half the chapters are an anthology of Jackson's past writings, exemplifying the clarity, wisdom, and wit for which he is so well known. The other half of the book is new: Jackson and his colleagues give their latest views on requirements, specifications, design, problem frames, and programming methods. Although many people have observed that software engineering should be more of an engineering discipline, few have drawn from the wider engineering literature more deeply or usefully than Jackson. Because of his work, many software engineers have a better perspective on their software and the real world it is intended to serve. Click here to order.

Personal Information

Last updated February 2024.