Refinement. Semantics, Languages and Applications

Contents......Page 3
Motivation......Page 8
--- Semantics......Page 15
1.1 Introduction......Page 16
1.2 Labelled Transition Systems – A Simple Model  of Computation......Page 17
1.3 Trace Refinement......Page 20
1.4 Completed Trace Refinement......Page 24
1.5 Failures Refinement......Page 25
1.6 Readiness Refinement......Page 29
1.7 Failure Trace Refinement......Page 30
1.9 Conformance and Extension......Page 31
1.10.1 Adding Data......Page 34
1.10.2 Infinite Trace Refinement......Page 35
1.11 Summary......Page 36
1.12 Bibliographical Notes......Page 37
References......Page 39
2.1 Introduction......Page 40
2.2 Refinement and Simulations......Page 42
2.2.1 Forward and Backward Simulations......Page 43
2.2.2 Completeness Results......Page 47
2.3 Bisimulation......Page 49
2.4 Bibliographical Notes......Page 50
References......Page 51
3.1 Introduction......Page 52
3.2 A Basic Model with Refinement......Page 53
3.3 Termination and Refinement......Page 54
3.4 More than One Observation......Page 55
3.5 Towards Total Correctness......Page 56
3.6 Observations Including Initial States......Page 57
3.7 State Abstraction......Page 58
3.8 State Variables and Observation......Page 60
3.9 Programs and Labeled Transitions......Page 61
References......Page 62
4 Relational View of Refinement......Page 63
4.1 Introduction......Page 64
4.2 Relational Data Types......Page 65
4.3 Relational Refinement......Page 67
4.4.1 Partial Relations and Their Totalisation......Page 71
4.4.2 Simulation Rules......Page 74
4.4.3 Completeness of Partial Relational Simulations......Page 75
4.4.4 A Fully Partial Relational Theory......Page 77
4.5 Bibliographical Notes......Page 78
References......Page 79
5 Perspicuity, Divergence & Internal Operations......Page 80
5.1 Perspicuous Operations......Page 81
5.2 Error Behaviour: Catastrophic or Not?......Page 83
5.3 Divergence......Page 84
5.4 Internal Operations......Page 86
5.4.1 Internal Operations and Choice in LTS......Page 87
5.4.2 Internal Actions in a Relational Context......Page 89
5.4.3 Divergence from Internal Operations......Page 90
References......Page 91
--- Refinement in Specification Languages......Page 93
6.1 CSP - The Language......Page 94
6.1.1 Sequential Operators......Page 95
6.1.2 Building Concurrent Specifications......Page 98
6.2 CSP - The Semantics......Page 102
6.2.1 The CSP Failures Model......Page 105
6.2.2 The CSP Failures, Divergences and Infinite Traces Semantics......Page 109
6.3 CSP - Refinement......Page 113
6.3.1 Trace Refinement......Page 114
6.3.2 Stable Failures Refinement......Page 115
6.3.3 FDI Refinement......Page 116
6.4.1 The LOTOS Language......Page 117
6.4.2 LOTOS Semantics and Refinement......Page 119
6.5.1 The CCS Language......Page 123
6.5.2 CCS Semantics and Refinement......Page 125
6.6 Bibliographical Notes......Page 128
References......Page 129
7.1 Z - The Language......Page 130
7.1.1 Using Schemas......Page 131
7.1.2 The Z Schema Calculus......Page 133
7.2.1 The Relational Semantics of a Z Specification......Page 135
7.2.2 Data Refinement and Simulations for Z......Page 136
7.2.3 Z Refinement in Practice......Page 139
7.3 The B-Method......Page 144
7.3.1 Machine Consistency......Page 146
7.4 Refinement in the B-Method......Page 148
7.4.1 Proof Obligations for Refinement......Page 150
7.4.2 Implementation Machines......Page 152
7.5 Bibliographical Notes......Page 153
References......Page 154
8.1 Event-B......Page 157
8.1.1 Specifying Machines in Event-B......Page 158
8.1.2 Proof Obligations for Event-B Machines......Page 159
8.2 Refinement in Event-B......Page 160
8.2.1 A Relational Semantics for Event-B......Page 162
8.2.2 Data Refinement and Simulations for Event-B......Page 166
8.3 ASM......Page 176
8.3.1 ASM Semantics and ASM Refinement......Page 177
8.4 Bibliographical Notes......Page 182
References......Page 184
--- Relating Notions of Refinement......Page 185
9.1 Introduction......Page 186
9.2 Background......Page 187
9.3 Relating Process Algebraic and Relational Refinement......Page 188
9.3.1 Trace Refinement......Page 190
9.3.2 Completed Trace Refinement......Page 192
9.3.3 Failure Refinement......Page 195
9.3.4 Failure Trace Refinement......Page 196
9.3.5 Extension and Conformance......Page 197
9.4 Relating Data Refinement to Process Algebraic Refinement......Page 199
9.4.1 Non-blocking Data Refinement and the Traces-Divergences Semantics......Page 201
9.4.2 Blocking Data Refinement and the Singleton Failures Semantics......Page 202
9.5 Relating Automata and Relational Refinement......Page 203
9.5.1 IO Automata......Page 204
9.6 Internal Events and Divergence......Page 208
9.7 Bibliographical Notes......Page 209
References......Page 211
10.2 The Basic Relational Embedding......Page 213
10.3 Dealing with Input and Output......Page 217
10.3.1 Defining the Extended Finalisation......Page 218
10.3.2 Deriving the New Simulation Rules......Page 220
10.3.3 An Example......Page 229
10.4 Summary of Simulation Conditions......Page 232
10.4.1 Discussion......Page 234
10.5 Bibliographical Notes......Page 237
References......Page 238
11.1 Introduction......Page 240
11.2 A Relational ADT with Divergence and Blocking......Page 242
11.2.1 Forward Simulation for Process Data Types......Page 244
11.2.2 Backward Simulation for Process Data Types......Page 246
11.3.1 Embedding a Basic Data Type with Internal Operations into a Process Data Type......Page 248
11.3.2 Correctness of the Embedding: Blocking Approach......Page 251
11.3.3 Simulations in the Blocking Approach......Page 253
11.3.4 The Non-blocking Approach......Page 256
11.4.1 Refinement Conditions for Output Embeddings......Page 259
11.4.2 Outputs in the Blocking Approach......Page 260
11.4.3 Outputs in the Non-blocking Approach......Page 263
References......Page 266
12 Conclusions......Page 267
References......Page 271