Description
Book SynopsisThe CSP approach has been widely used in the specification, analysis and verification of concurrent and real-time systems, and for understanding the particular issues that can arise when concurrency is present. It provides a language which enables specifications and designs to be clearly expressed and understood, together with a supporting theory which allows them to be analyzed and shown to be correct.
This book supports advanced level courses on concurrency covering timed and untimed CSP. The first half introduces the language of CSP, the primary semantic models (traces, failures, divergences and infinite traces), and their use in the modelling, analysis and verification of concurrent systems. The second half of the book introduces time into the language, brings in the timed semantic model (timed failures) and finally presents the theory of timewise refinement which links the two halves together.
Accompanying website: http://www.cs.rhbnc.ac.uk/books/concurre
Table of ContentsPreface ix
Acknowledgements xv
Part 1 The language of CSP
1 Sequential processes 3
1.1 Events and processes 3
1.2 Performing events 8
1.3 Recursion 13
1.4 Choice 20
2 Concurrency 31
2.1 Alphabetized parallel 31
2.2 Interleaving 44
2.3 Interface parallel 50
3 Abstraction and control flow 55
3.1 Hiding 55
3.2 Event renaming 62
3.3 Sequential composition 69
3.4 Interrupt 72
3.5 Notes 74
Part II Analysing processes
4 Traces 87
4.1 Sequences 87
4.2 Trace semantics 91
4.3 Recursion 117
4.4 Testing 133
4.5 Congruence 136
5 Specification and verification with traces 141
5.1 Property-oriented Specification 141
5.2 Verification 143
5.3 Recursion induction 155
5.4 Case study: Distributed sum 160
5.5 Process-oriented specification 168
6 Stable failures 173
6.1 Observing processes 174
6.2 Process semantics 178
6.3 Recursion 188
7 Specification and verification with failures 195
7.1 Property-oriented specification 195
7.2 Verification 197
7.3 Recursion induction 206
7.4 Process-oriented specification 209
7.5 Case study: Distributed sum 212
8 Failures, divergences, and infinite traces 221
8.1 Observing processes 221
8.2 Process semantics 229
8.3 Recursion 242
8.4 Specification and verification 248
8.5 Recursion induction 253
8.6 Case study: Distributed sum 256
8.7 Must testing and FDI equivalence 257
8.8 Notes 258
Part III Introducing time
9 The timed language 267
9.1 Timed computational model 268
9.2 Transitions 269
9.3 Performing events 270
9.4 Choice 275
9.5 Recursion 286
9.6 Concurrency 290
9.7 Abstraction 297
9.8 Flow of control 304
10 Timed transition systems 313
10.1 Evolution 313
10.2 Executions 315
10.3 Well-timed processes 327
10.4 Notes 329
Part IV Timed analysis
11 Semantics of timed CSP 335
11.1 Timed observations 336
11.2 Timed failures semantics 347
11.3 Recursion 358
11.4 Testing and timed failures equivalence 363
12 Timed specification and verification 369
12.1 Specification 369
12.2 Verification 375
12.3 Recursion induction 385
12.4 Ill-timed processes 388
12.5 Case study: Fischer’s protocol 390
13 Timewise refinement 399
13.1 Trace timewise refinement 400
13.2 Failures timewise refinement 410
13.3 Refinement and parallel composition 413
13.4 Case study: a railway crossing 431
13.5 FDI timewise refinement 436
13.6 Testing and timewise refinement 439
13.7 Notes 442
Appendix A: Event-based time 447
A.1 Standard CSP and took 448
A.2 Translating from timed CSP 454
A.3 Notes 465
Appendix B: Model-checking with FDR 469
B.1 Interacting with FDR 470
B.2 How FDR checks refinement 473
B.3 Machine readable CSP 478
References 485
Notation 493
Index 498
Index of Processes 507
