Validated Designs for Object-Oriented Systems

Contents......Page 3
Part I: Models and Software Development......Page 7
1.1 The Challenge of Software Development......Page 8
1.2 Mastering Complexity: The Role of Modelling......Page 9
1.3 The Place of Modelling in Software Development......Page 10
1.4 Modelling Structure: Object-oriented Systems......Page 11
1.5 Modelling Data and Functionality: VDM++......Page 15
1.6 Using VDM++ in Object-oriented Design......Page 19
1.7 Book Organisation and Content......Page 20
1.7.1 Conventions Used in This Book......Page 21
1.7.2 Overview of Examples......Page 22
1.8 Summary......Page 23
2.1 Constructing a Model......Page 24
2.2 A Chemical Plant Example......Page 25
2.3.1 Creating a Dictionary......Page 26
2.3.2 Sketching Class Representations......Page 27
2.3.3 Sketching Signatures for Operations......Page 33
2.4 Making the Model More Comprehensive......Page 34
2.4.1 Adding Invariant Properties......Page 35
2.4.2 Completing Operation Definitions......Page 36
2.4.3 Constructing Instances......Page 40
2.5 Validating the Model......Page 43
2.5.2 Automated Validation Using Systematic Testing......Page 44
2.5.3 Visual Validation Using Rapid Prototyping......Page 45
2.7 Summary......Page 46
3.1 Introduction......Page 47
3.3 Using Rose......Page 48
3.4 Using VDMTools......Page 51
3.4.3 Setting Tool Options......Page 52
3.4.4 Type Checking......Page 53
3.4.5 Mapping Back to Rose......Page 55
3.4.7 Interpreting VDM++ Models......Page 56
3.4.8 Setting Project Options and Breaking Conditions......Page 59
3.4.9 Integrity Checking......Page 60
3.4.10 A Command-Line Interface......Page 62
3.5 Summary......Page 64
Part II: Modelling Object-oriented Systems in VDM++......Page 65
4.1 Introduction......Page 66
4.2 Object-oriented Structuring......Page 67
4.2.1 Visibility Rules......Page 70
4.3 Instance Variables and Invariants......Page 71
4.4.1 Basic Types......Page 74
4.4.2 Constructed Types......Page 76
4.4.3 Type Definitions......Page 82
4.4.4 Invariants on Type Definitions......Page 83
4.4.5 Types in the EPR Example......Page 84
4.5 Values and Value Definitions......Page 86
4.6 Summary......Page 87
5.1 Introduction......Page 88
5.2.1 Implicit Function Definitions......Page 89
5.2.2 Explicit Function Definitions......Page 91
5.3.1 Implicit Operation Definitions......Page 94
5.3.2 Explicit Operation Definitions......Page 95
5.3.4 Constructors......Page 98
5.4.1 Let and Def Expressions......Page 100
5.4.2 Conditional Expressions......Page 101
5.4.4 Record Expressions......Page 102
5.5 Pattern Binding......Page 103
5.6 Bindings......Page 104
5.7 Statements......Page 105
5.7.2 The Assignment Statement......Page 106
5.7.4 Loop Statements......Page 107
5.8 Summary......Page 108
6.2 Overview of Sets......Page 110
6.3 The Robot Controller......Page 114
6.3.1 Points and Routes......Page 116
6.3.2 Using Sets of Points......Page 120
6.3.3 Arriving at a Waypoint......Page 121
6.3.4 Controlling the Robot......Page 125
6.3.5 More about Routes......Page 128
6.3.6 Avoidance Routes......Page 131
6.3.7 Review......Page 135
6.3.8 Extending the Robot Controller......Page 136
6.4 Summary......Page 138
7.2 Overview of Sequences......Page 139
7.3 The Congestion Warning System (CWS)......Page 144
7.3.1 Sensors......Page 152
7.3.3 Actuators......Page 158
7.3.4 Class OperatorControl......Page 163
7.4 Summary......Page 167
8.2 Overview of Mappings......Page 168
8.3 The Congestion Warning System Revisited......Page 172
8.3.1 Sensors and Traffic Controls......Page 180
8.3.2 Actuators......Page 182
8.3.3 Operator Control......Page 188
8.4 Summary......Page 189
Part III: Modelling in Practice: Three Case Studies......Page 190
9.1 Introduction......Page 191
9.2 The Historic Significance of Enigma......Page 192
9.3 The Enigma Cipher Algorithm......Page 193
9.4 Building the Enigma Model......Page 195
9.4.1 Alphabet......Page 198
9.4.2 Component......Page 200
9.4.3 Configuration......Page 202
9.4.4 Reflector......Page 204
9.4.5 Rotor......Page 206
9.4.6 Plugboard......Page 210
9.4.7 Enigma......Page 212
9.5 The VDMUnit Framework......Page 214
9.5.1 Test......Page 218
9.5.2 TestSuite......Page 219
9.5.3 TestCase......Page 220
9.5.4 TestResult......Page 223
9.6.1 PlugboardTest......Page 224
9.6.2 SimpleEnigmaTest......Page 226
9.6.3 EnigmaTest......Page 227
9.7 Summary......Page 229
10.1 Introduction......Page 230
10.2 The CSLaM System......Page 231
10.3 The On-board CSL System......Page 232
10.4 Member Declarations......Page 233
10.5 The Cab Display......Page 235
10.6 The Beacon Classes......Page 237
10.7 Announcements and Restrictions......Page 239
10.8 Monitoring the Performance of Drivers......Page 240
10.9 Summary......Page 245
11.1 Introduction......Page 248
11.2.1 What Is Architecture?......Page 250
11.2.2 Developing Enterprise Architectures......Page 251
11.2.3 An Example: A Four-Tier Enterprise Architecture......Page 252
11.3 The TradeOne Architecture......Page 254
11.3.1 The Database Architecture in Detail......Page 256
11.3.2 The Business Logic Architecture......Page 260
11.4 The Validation Approach......Page 263
11.5.1 Overall Size of TradeOne......Page 264
11.5.2 The Development Team and Project Time Scales......Page 266
11.5.3 Defect Metrics......Page 268
11.6 Lessons Learned from the TradeOne Project......Page 269
11.7 Summary......Page 270
Part IV: From Models to Code......Page 272
12.1 Introduction......Page 273
12.2.1 Threads......Page 274
12.2.2 Permission Predicates......Page 275
12.3.1 Overview......Page 280
12.3.2 The POP3Server Class......Page 281
12.3.3 Client Handler States......Page 283
12.3.4 Starting a Client Session......Page 284
12.3.5 Interacting with the Client......Page 285
12.4 Synchronising Communication in the POP3 Server......Page 289
12.5 Summary......Page 292
13.1 Introduction......Page 293
13.2 Assessing Internal Consistency: Integrity Checking......Page 294
13.2.1 Machine-Assisted Checking: Formal Integrity Properties......Page 296
13.3.1 Introduction to the API......Page 301
13.3.2 Connecting to the API......Page 302
13.3.3 Interacting with the API......Page 303
13.4 Validating the POP3 Example through the API......Page 305
13.4.2 Interacting with One Client......Page 306
13.4.4 Interaction between Client and Server......Page 308
13.4.6 Closing the POP3 Session......Page 313
13.4.7 Interacting with Multiple Clients......Page 314
13.5 Summary......Page 315
14.1 Introduction......Page 317
14.2.3 Handwritten Parts......Page 318
14.2.4 VDM.jar......Page 319
14.3 Basic Code Generation......Page 320
14.3.1 Keep Tags......Page 324
14.3.2 Options for Java Code Generation......Page 326
14.4.1 Permission Predicates......Page 332
14.4.2 Threads......Page 335
14.5.1 Overview of Server Side......Page 337
14.5.2 Overview of Client Side......Page 340
14.6 Summary......Page 341
Appendices......Page 344
Solutions for Chapter 4......Page 345
Solutions for Chapter 5......Page 351
Solutions for Chapter 6......Page 352
Solutions for Chapter 7......Page 357
Solutions for Chapter 8......Page 361
Solutions for Chapter 9......Page 365
Solutions for Chapter 10......Page 367
Solutions for Chapter 12......Page 374
Solutions for Chapter 13......Page 376
Solutions for Chapter 14......Page 378
References......Page 379
List of Acronyms......Page 382
Subject Index......Page 384
Definitions Index......Page 393