Refinement. Semantics, Languages and Applications

Description

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