Process algebra is a widely accepted and much used technique
in the specification and verification of parallel and distributed
software systems. This book assembles the relevant results of
most process algebras currently in use, and presents them in
a unified framework and notation.
The book describes the theory underlying the development, realization and maintenance of software that occurs in parallel or distributed systems. A system can be specified in the syntax provided, and the axioms can be used to verify that a composed system has the required external behavior. As examples, two protocols are completely specified and verified in the text: the Alternating-Bit Protocol for Data Communication, and Fischer's Protocol of Mutual Exclusion. The book serves as a reference text for researchers and graduate students in computer science, offering a complete overview of the field and referring to further literature where appropriate. It contains over 300 exercises ranging in difficulty to suit all readers.
"Its crowning achievement is to exploit the unifying power of algebra to cover a range of historic theories." Tony Hoare
"The presentation is lucid and careful, enriched with exercises." Robin Milner
"This book will definitely be useful as a reference work for research in process theory." Jan Bergstra
Foreword by Tony Hoare | |
Foreword by Robin Milner | |
Foreword by Jan Bergstra | |
Preface | |
1. | Process algebra |
2. | Preliminaries |
3. | Transition systems |
4. | Basic process theory |
5. | Recursion |
6. | Sequential processes |
7. | Parallel and communicating processes |
8. | Abstraction |
9. | Timing |
10. | Data and states |
11. | Features |
12. | Semantics |
Bibliography | |
Index of Symbols and Notations | |
Index of Authors | |
Index of Subjects |
Jos Baeten, Twan Basten, and Michel Reniers, all from Eindhoven University of Technology, are experts in the field of Process Algebra and computational models in general. They are experienced teachers and writers. Building upon the work of many others, they have made an attempt to bring together the dominating process algebraic theories in a unifying framework and notation, as an aid to both researchers and teachers interested in this field.