Process algebra is a widely accepted and much used technique in the specification and verification of parallel and distributed software systems. This book sets the standard for the field. It assembles the relevant results of most process algebras currently in use, and presents them in a unified framework and notation. The authors describe 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.
Author(s): J. C. M. Baeten, T. Basten, M. A. Reniers
Series: Cambridge Tracts in Theoretical Computer Science 50
Publisher: CUP
Year: 2010
Language: English
Pages: 478
Half-title......Page 3
Series-title......Page 4
Title......Page 5
Copyright......Page 6
Contents......Page 7
Tony Hoare......Page 11
Robin Milner......Page 12
Jan Bergstra......Page 13
What is this book about?......Page 15
How to use this book?......Page 16
Acknowledgements......Page 17
1.1 Definition......Page 19
1.2 Calculation......Page 21
1.3 History......Page 22
Bekic......Page 23
CCS......Page 24
CSP......Page 25
ACP......Page 26
This book......Page 27
Bibliographical remark......Page 28
2.2 Equational theories......Page 29
2.3 Algebras......Page 39
2.4 Term rewriting systems......Page 48
2.5 Bibliographical remarks......Page 52
3.1 Transition-system spaces......Page 53
3.2 Structural operational semantics......Page 65
3.3 Bibliographical remarks......Page 82
4.1 Introduction......Page 85
4.2 The process theory MPT......Page 86
4.3 The term model......Page 90
4.4 The empty process......Page 99
4.5 Projection......Page 110
4.6 Prefix iteration......Page 120
4.7 Bibliographical remarks......Page 125
5.1 Introduction......Page 127
5.2 Recursive specifications......Page 128
5.3 Solutions of recursive specifications......Page 131
5.4 The term model......Page 137
5.5 Recursion principles......Page 142
5.6 Describing a stack......Page 164
5.7 Expressiveness and definability......Page 166
5.8 Regular processes......Page 172
5.9 Recursion and BSP*(A)
......Page 175
5.10 The projective limit model......Page 177
5.11 Bibliographical remarks......Page 186
6.2 The process theory TSP......Page 189
6.3 The term model......Page 192
6.4 Projection in TSP(A)......Page 195
6.5.1 Prefix iteration......Page 196
6.5.2 General iteration......Page 197
6.6.1 The theory......Page 200
6.6.2 The stack revisited......Page 202
6.6.3 Some expressiveness aspects......Page 204
6.7 Renaming, encapsulation, and skip operators......Page 207
6.8 Bibliographical remarks......Page 212
7.1 Interleaving......Page 213
7.2 An operational view......Page 214
7.3 Standard communication......Page 217
7.4 The process theory BCP......Page 219
7.5 The term model......Page 234
7.6 Recursion, buffers, and bags......Page 236
7.7 The process theory TCP and further extensions......Page 245
7.8 Specifying the Alternating-Bit Protocol......Page 253
7.9 Bibliographical remarks......Page 260
8.1 Introduction......Page 263
8.2 Transition systems with silent steps......Page 264
8.3 BSP with silent steps......Page 274
8.4 The term model......Page 276
8.5 Some extensions of BSPτ(A)......Page 285
8.5.1 Abstraction......Page 286
8.5.2 Encapsulation......Page 288
8.5.3 Projection......Page 289
8.5.4 Non-determinism in CSP......Page 290
8.6 TCP with silent steps......Page 294
8.7 Iteration and divergence......Page 298
8.8 Recursion and fair abstraction......Page 302
8.9 Verification of the ABP and queues revisited......Page 313
8.10 Bibliographical remarks......Page 316
9.1 Introduction......Page 319
9.2 Timed transition systems......Page 322
9.3 Discrete time, relative time......Page 325
9.4 The term model......Page 327
9.5 Time iteration and delayable actions......Page 330
9.6 The relation between BSP(A) and BSPdrt*(A)......Page 335
9.7 The process theory TCPdrt*(A, γ)......Page 337
9.8 Fischer's protocol......Page 345
9.9 Bibliographical remarks......Page 351
10.1 Introduction......Page 353
10.2 Guarded commands......Page 354
10.3 The inaccessible process......Page 363
10.4 Propositional signals......Page 366
10.5 State operators......Page 380
10.6 Choice quantification......Page 384
10.7 Bibliographical remarks......Page 392
11.1 Priorities......Page 393
11.2 Probabilities......Page 399
11.3 Mobility......Page 405
11.4 Parallel composition revisited......Page 407
11.5 Bibliographical remarks......Page 409
12.1 Bisimilarity and trace semantics......Page 411
12.2 Failures and readiness semantics......Page 415
12.3 The linear time – branching time lattice......Page 419
12.4 Partial-order semantics......Page 425
12.5 Bibliographical remarks......Page 428
Bibliography......Page 429
Index of Symbols and Notations......Page 439
Index of Authors......Page 453
Index of Subjects......Page 457
