Reactive systems: modelling, specification and verification

Cover
......Page 1
Reactive Systems......Page 2
Reactive Systems - Modelling, Specification and Verification......Page 4
ISBN-10: 0521875463  ISBN-13: 9780521875462  ISBN-10: 0511335350  ISBN-13: 9780511335358......Page 5
Contents......Page 6
Figures......Page 9
Tables......Page 10
Preface......Page 11
Aims of this book......Page 18
1.1 What are reactive systems?......Page 19
1.2 Process algebras......Page 22
2.1 Some CCS process constructions......Page 24
2.1.1 The behaviour of processes......Page 31
2.2 CCS, formally......Page 33
2.2.1 The model of labelled transition systems......Page 34
2.2.2 The formal syntax and semantics of CCS......Page 38
2.2.3 Value-passing CCS......Page 45
3.1 Criteria for good behavioural equivalence......Page 48
3.2 Trace equivalence: a first attempt......Page 51
3.3 Strong bisimilarity......Page 53
3.4 Weak bisimilarity......Page 70
3.5 Game characterization of bisimilarity......Page 82
3.5.1 Weak bisimulation games......Page 87
3.6 Further results on equivalence checking......Page 89
4.1 Posets and complete lattices......Page 92
4.2 Tarski's fixed point theorem......Page 95
4.3 Bisimulation as a fixed point......Page 102
5.1 Introduction to Hennessy–Milner logic......Page 106
5.2 Hennessy–Milner theorem......Page 115
Introduction......Page 119
6.1 Examples of recursive properties......Page 124
6.2 Syntax and semantics of HML with recursion......Page 126
6.3 Largest fixed points and invariant properties......Page 130
6.4 A game characterization for HML with recursion......Page 132
6.4.1 Examples of use......Page 134
6.5 Mutually recursive equational systems......Page 137
6.6 Characteristic properties......Page 142
6.7 Mixing largest and least fixed points......Page 151
6.8 Further results on model checking......Page 156
Introduction......Page 159
7.1 Specifying mutual exclusion in HML......Page 164
7.2 Specifying mutual exclusion using CCS itself......Page 166
7.3 Testing mutual exclusion......Page 169
8.1 Real-time reactive systems......Page 176
9.1 Intuition......Page 178
9.2 Timed labelled transition systems......Page 180
9.3 Syntax and SOS rules of timed CCS......Page 182
9.4 Parallel composition......Page 186
9.5 Other timed process algebras and discussion......Page 190
10.1 Motivation......Page 192
10.2 Syntax of timed automata......Page 193
10.3 Semantics of timed automata......Page 197
10.4 Networks of timed automata......Page 202
10.5 More on timed-automata formalisms......Page 207
11.1 Timed and untimed trace equivalence......Page 210
11.2 Timed and untimed bisimilarity......Page 212
11.3 Weak timed bisimilarity......Page 217
11.4 Region graphs......Page 220
11.5 Zones and reachability graphs......Page 231
11.6 Further results on timed equivalences......Page 235
Introduction......Page 237
12.1 Basic logic......Page 238
12.2 Hennessy–Milner logic with time and regions......Page 246
12.3 Timed bisimilarity versus HML with time......Page 249
12.4 Recursion in HML with time......Page 254
12.4.1 Characteristic properties for timed bisimilarity......Page 258
12.4.2 Examples of real-time temporal properties......Page 262
12.5 More on timed logics......Page 263
Introduction......Page 265
13.1 Mutual exclusion using timing......Page 267
13.2 Modelling Fischer's algorithm......Page 268
13.2.1 Proving mutual exclusion using UPPAAL......Page 270
13.2.2 An erroneous version of Fischer's algorithm......Page 273
13.3 Further exercises on timing-based mutual exclusion algorithms......Page 275
A.1 Alternating-bit protocol......Page 278
A.2 Gossiping girls......Page 279
A.3 Implementation of regions......Page 280
References......Page 284
Index......Page 298