A new approach for the design and description of distributed programming and reactive systems is presented. The book provides a new notation called interacting processes (IP), used to express the design of reactive systems. In addition to the theoretical foundation, the authors illustrate the approach with design and programming examples and case studies to illustrate their method. The book’s main audience is software engineers involved in developing distributed systems. Researchers and students learning about formal methods of software design will also find the book useful.
The book is divided into ten chapters. Chapter 1 introduces the underlying reasons for this new approach. This chapter also summarizes the main ideas of IP notation and distinguishes IP as viewing a reactive system as a collection of interacting processes. IP bases the interprocess relationships on synchronous multiparty interactions as the sole means of interprocess communication and synchronization.
Chapter 2, “The IP Core Language,” begins with informal definitions of the language constructs followed by the formal semantics of IP. Several examples demonstrate parts of the language. Chapter 3, “Abstraction,” uses abstraction to modularize the IP language and discusses the use of a construct called a “team” to abstract and encapsulate multiparty activities. This chapter includes a number of examples that illustrate the different features of the IP language and concludes with an IP solution to the lift (elevator) problem. Chapter 4, “Proving Properties of IP Programs,” focuses on the details involved in designing proof systems for some of the IP language constructs. Chapter 5, “Fairness,” focuses on different fairness assumptions for multiparty interactions.
Chapter 6, “Superimposition,” discusses an adaptation of superimposition, which is the second major modularization tool of the IP language. This chapter concludes with an example of IP applied to the algorithm for leader election. Chapter 7, “Refinement in IP,” focuses on a collection of synchrony-loosening transformations for multiparty interactions. Chapter 8, “Implementing Multiparty Interactions,” surveys several algorithms that solve the coordinating problem, which deals with presynchronization in implementing multiparty interactions. Chapter 9, “Related Works,” uses several other notations that have multiparty synchronization to express a debit card system that is discussed in an earlier chapter. The final chapter, “Conclusions,” considers the importance of IP and briefly discusses several of its uses, including software systems design, programming languages, and groupware.
The book has extensive references to earlier research in distributed computing and distributed systems, as well as to literature discussing notations similar to IP. It is very well written and includes a large number of examples to illustrate many of the more difficult concepts. Though challenging to read, it is well suited for anyone interested in distributed programming.