Real Time Programming: Languages, Specification & Verification

Contents......Page 12
Preface......Page 6
Organization of the Monograph......Page 8
Dependence of the chapters......Page 9
Acknowledgement......Page 10
Summary......Page 18
1 Real Time System Characteristics......Page 20
1.1 Real-time and Reactive Programs......Page 21
2 Formal Program Development Methodologies......Page 26
2.1 Requirement Specification......Page 27
2.1.1 An Example......Page 29
2.2 System Specifications......Page 30
3 Characteristics of Real-Time Languages......Page 34
3.1 Modelling Features of Real-Time Languages......Page 36
3.2 A Look at Classes of Real-Time Languages......Page 39
4 Programming Characteristics of Reactive Systems......Page 42
4.2 Perfect Synchrony Hypothesis......Page 43
4.4 Logical Concurrency and Broadcast Communication......Page 44
4.5 Determinism and Causality......Page 45
Summary......Page 46
5.1 Top Level Structure......Page 48
5.1.1 Signals and Events......Page 49
5.1.2 Module Instantiation......Page 50
5.2 Esterel Statements......Page 51
5.2.2 Reactive Statements......Page 53
5.2.3 Derived Statements......Page 58
5.3 Illustrations of Esterel Program Behaviour......Page 60
5.4 Causality Problems......Page 62
5.5 A Historical Perspective......Page 63
6.1 A Simulation Environment......Page 66
6.2 Verification Environment......Page 69
7.1.1 A Very Simple Auto Controller......Page 72
7.1.2 A Complex Controller......Page 73
7.1.3 A Cruise Controller......Page 75
7.1.4 A Train Controller......Page 78
7.1.5 A Mine Pump Controller......Page 80
8 Asynchronous Interaction in Esterel......Page 84
9.1 Arbitration Process......Page 88
9.2 Abstraction of the Protocol......Page 89
9.3 Solution in Esterel......Page 91
10.1 Semantic Structure......Page 96
10.2 Transition Rules......Page 98
10.2.1 Rules for Signal Statement......Page 101
10.3 Illustrative Examples......Page 104
10.4 Discussions......Page 106
10.5 Semantics of Esterel with exec......Page 107
Summary......Page 112
11.2 Flows and Streams......Page 114
11.3 Equations, Variables and Expressions......Page 115
11.4 Program Structure......Page 116
11.4.1 Illustrative Example......Page 118
11.5 Arrays in Lustre......Page 119
11.6.2 A Complex Controller......Page 120
11.6.3 A Cruise Controller......Page 121
11.6.4 A Train Controller......Page 123
11.6.5 A Mine Pump Controller......Page 124
12.1 Time-Triggered Protocol......Page 128
12.1.1 Clock Synchronization......Page 130
12.1.2 Bus Guardian .......Page 131
12.2 Modelling TTP in Lustre......Page 132
13.1 Argos Constructs......Page 140
13.2 Illustrative Example......Page 142
13.3 Discussions......Page 145
Summary......Page 148
14.1 Transition System Based Veri cationy of Esterel Programs......Page 150
14.1.1 Detailed Discussion......Page 151
14.2 Esterel Transition System......Page 152
14.2.1 Abstraction and Hiding......Page 153
14.2.2 Observation Equivalence Reduction......Page 155
14.2.3 Context Filtering......Page 156
14.3 Temporal Logic Based Verification......Page 157
14.4 Observer-based Verification......Page 158
14.5 First Order Logic Based Verification......Page 160
15.1 A Simple Auto Controller......Page 162
15.3 A Cruise Controller......Page 163
15.4 A Train Controller......Page 164
15.5 A Mine Pump Controller......Page 165
Summary......Page 166
16.1 An Overview of CRP......Page 168
16.2 Communicating Reactive Processes: Structure......Page 170
16.2.1 Syntax of CRP......Page 171
16.2.2 Realizing Watchdog Timers in CRP......Page 172
16.3 Behavioural Semantics of CRP......Page 173
16.4 An Illustrative Example: Banker Teller Machine......Page 174
16.5 Implementation of CRP......Page 177
17.1 A Brief Overview of CSP......Page 182
17.2 Translation of CSP to CRP......Page 183
17.5 Ready-Trace Semantics of CSP......Page 185
17.5.3 Semantics of `send' Action......Page 187
17.5.7 Semantics of Guarded Selection......Page 188
17.6.1 Behavioural Traces of CRP Programs......Page 189
17.7 Correctness of the Translation......Page 191
17.8 Translation into meije Process Calculus......Page 193
18 Communicating Reactive State Machines......Page 198
18.1 CRSM Constructs......Page 199
18.2 Semantics of CRSM......Page 200
19.1 Need for a Multiclock Synchronous Paradigm......Page 204
19.2 Informal Introduction......Page 206
19.2.1 Latched Signals......Page 208
19.2.2 Expressions......Page 209
19.2.3 Multiclock Esterel Statements......Page 210
19.2.4 Informal Development of Programs in Multiclock Esterel......Page 211
19.3.1 Specification of Clocks......Page 214
19.4 Embedding CRP......Page 229
19.5 Modelling a VHDL Subset......Page 235
19.6 Discussion......Page 236
20 Modelling Real-Time Systems in Esterel......Page 238
20.2.1 Deadline Specification......Page 239
20.2.2 Periodic Activities......Page 240
20.2.3 Guaranteed Activities......Page 241
21 Putting it Together......Page 248
Bibliography......Page 252
Index......Page 260
Summary......Page 11