search for books and compare prices
Tables of Contents for Concurrent and Real-Time Systems
Chapter/Section Title
Page #
Page Count
Preface
ix
 
Acknowledgements
xv
 
Part I The language of CSP
Sequential processes
3
28
Events and processes
3
5
Performing events
8
5
Recursion
13
7
Choice
20
11
Concurrency
31
24
Alphabetized parallel
31
13
Interleaving
44
6
Interface parallel
50
5
Abstraction and control flow
55
32
Hiding
55
7
Event renaming
62
7
Sequential composition
69
3
Interrupt
72
2
Notes
74
13
Part II Analysing processes
Traces
87
54
Sequences
87
4
Trace semantics
91
26
Recursion
117
16
Testing
133
3
Congruence
136
5
Specification and verification with traces
141
32
Property-oriented Specification
141
2
Verification
143
12
Recursion induction
155
5
Case study: Distributed sum
160
8
Process-oriented specification
168
5
Stable failures
173
22
Observing processes
174
4
Process semantics
178
10
Recursion
188
7
Specification and verification with failures
195
26
Property-oriented specification
195
2
Verification
197
9
Recursion induction
206
3
Process-oriented specification
209
3
Case study: Distributed sum
212
9
Failures, divergences, and infinite traces
221
46
Observing processes
221
8
Process semantics
229
13
Recursion
242
6
Specification and verification
248
5
Recursion induction
253
3
Case study: Distributed sum
256
1
Must testing and FDI equivalence
257
1
Notes
258
9
Part III Introducing time
The timed language
267
46
Timed computational model
268
1
Transitions
269
1
Performing events
270
5
Choice
275
11
Recursion
286
4
Concurrency
290
7
Abstraction
297
7
Flow of control
304
9
Timed transition systems
313
22
Evolution
313
2
Executions
315
12
Well-timed processes
327
2
Notes
329
6
Part IV Timed analysis
Semantics of timed CSP
335
34
Timed observations
336
11
Timed failures semantics
347
11
Recursion
358
5
Testing and timed failures equivalence
363
6
Timed specification and verification
369
30
Specification
369
6
Verification
375
10
Recursion induction
385
3
Ill-timed processes
388
2
Case study: Fischer's protocol
390
9
Timewise refinement
399
48
Trace timewise refinement
400
10
Failures timewise refinement
410
3
Refinement and parallel composition
413
18
Case study: a railway crossing
431
5
FDI timewise refinement
436
3
Testing and timewise refinement
439
3
Notes
442
5
Appendix A: Event-based time
447
22
A.1 Standard CSP and tock
448
6
A.2 Translating from timed CSP
454
11
A.3 Notes
465
4
Appendix B: Model-checking with FDR
469
16
B.1 Interacting with FDR
470
3
B.2 How FDR checks refinement
473
5
B.3 Machine readable CSP
478
7
References
485
8
Notation
493
5
Index
498
9
Index of Processes
507