Real-Time Systems: Formal Specification and Automatic Verification

Cover......Page 1
Half-title......Page 3
Title......Page 5
Copyright......Page 6
Contents......Page 7
Structure of this book......Page 9
How to read this book......Page 10
Intended audience......Page 12
Courses based on this book......Page 13
Acknowledgements......Page 14
List of symbols......Page 17
1.1 What is a real-time system?......Page 19
1.2 System properties......Page 22
1.3.1 The problem......Page 25
1.3.2 Formalisation......Page 27
1.4.1 The problem......Page 30
1.4.2 Formalisation......Page 31
1.5 Aims of this book......Page 33
1.5.1 Duration Calculus......Page 34
1.5.2 Timed automata......Page 35
1.5.3 PLC-Automata......Page 36
1.5.4 Tying it all together......Page 37
1.6 Exercises......Page 38
1.7 Bibliographic remarks......Page 39
2.1 Preview......Page 46
2.2.1 Symbols......Page 49
2.2.2 State assertions......Page 51
2.2.3 Terms......Page 54
2.2.4 Formulas......Page 57
2.2.5 Validity, satisfiability, and realisability......Page 63
2.3 Specification and correctness proof......Page 65
2.3.1 Gas burner revisited......Page 67
2.4 Proof rules......Page 71
2.4.1 Predicate calculus......Page 75
2.4.2 Equality......Page 76
2.4.4 Interval logic......Page 79
2.4.5 Durations......Page 81
2.4.6 Induction......Page 82
2.4.7 Application to the gas burner......Page 86
Interval logic......Page 88
Modal operators......Page 89
Classic induction rule......Page 90
2.5 Exercises......Page 93
2.6 Bibliographic remarks......Page 97
3.1 Decidability results......Page 99
3.1.1 Decidability for discrete time......Page 100
Expressiveness of RDC......Page 101
Construction of L(F)......Page 102
Two-counter machines......Page 107
Reduction of two-counter machines to DC......Page 108
Discussion......Page 114
3.2 Implementables......Page 115
3.2.1 A controller for the gas burner......Page 121
3.2.2 Correctness proof......Page 123
3.3 Constraint Diagrams......Page 128
3.3.1 Syntax and semantics......Page 129
Phase sequence constraints......Page 133
Length requirements......Page 135
3.3.2 Generalised railroad crossing revisited......Page 138
3.3.3 A real-time filter......Page 140
3.3.4 Expressiveness......Page 143
3.4 Exercises......Page 146
3.5 Bibliographic remarks......Page 150
4.1 Timed automata......Page 152
4.2 Networks of timed automata......Page 163
4.3.1 Location reachability......Page 171
4.3.2 Constraint reachability......Page 181
4.4 The model checker UPPAAL......Page 183
4.4.1 Data variables......Page 184
4.4.3 Restricting nondeterminism......Page 186
4.4.4 Operational semantics of networks......Page 191
4.4.5 The logic of UPPAAL......Page 194
4.5 Exercises......Page 202
4.6 Bibliographic remarks......Page 205
5 PLC-Automata......Page 207
5.1 Programmable Logic Controllers......Page 208
5.2 PLC-Automata......Page 210
5.3 Translation into PLC source code......Page 215
5.4 Duration Calculus semantics......Page 219
5.4.1 Reaction times......Page 224
5.5 Synthesis from DC implementables......Page 230
5.5.1 Synthesis algorithm......Page 232
5.6.1 Hierarchical PLC-Automata......Page 245
5.6.2 Data and timer variables......Page 248
Parallel composition......Page 250
Sequential composition......Page 253
5.7 Exercises......Page 255
5.8 Bibliographic remarks......Page 258
6.1 The approach......Page 259
6.2 Requirements......Page 261
6.2.2 Constructing test automata......Page 262
Utility......Page 263
6.2.3 Discussion......Page 265
6.2.4 Automatically generated test automata......Page 266
Test automata for DC implementables......Page 268
Test automata for counterexample formulas......Page 273
6.3 Specification......Page 275
6.3.1 Railroad crossing......Page 276
6.3.2 Timed automata semantics of PLC-Automata......Page 280
6.4 Verification......Page 283
Verifying safety......Page 285
Verifying utility......Page 287
6.4.2 Discussion......Page 289
6.4.3 Separated assumptions......Page 291
Application to railroad crossing......Page 292
6.4.4 Plant, sensors, and actuators......Page 295
Application to railroad crossing......Page 296
6.5 The tool Moby/RT......Page 301
6.6 Summary......Page 305
6.7 Exercises......Page 307
6.8 Bibliographic remarks......Page 308
Logic......Page 311
Sets......Page 312
Relations......Page 313
Real numbers......Page 315
Words and languages......Page 316
Finite automata and regular languages......Page 317
Transition systems......Page 320
Bibliographic remarks......Page 321
Bibliography......Page 322
Index......Page 331