| Thematic Introduction | p. 1 |
| Specifications in Industry | p. 2 |
| Specification-Based Development | p. 3 |
| Overview of Formal Methods | p. 4 |
| Specification Case Studies in RAISE | p. 7 |
| Exemplified Themes | p. 11 |
| Lessons Learned | p. 16 |
| Introduction to RAISE | p. 19 |
| The RAISE Specification Language | p. 19 |
| The RAISE Method: Writing Initial Specifications | p. 51 |
| The RAISE Method: Developing Specifications | p. 62 |
| When Not to Use RAISE | p. 78 |
| A University Library Management System | p. 81 |
| Introduction | p. 81 |
| Requirements | p. 81 |
| Domain Analysis | p. 82 |
| Consistency | p. 92 |
| Functions | p. 94 |
| Conclusions | p. 97 |
| Development of a Distributed Telephone Switch | p. 99 |
| Introduction | p. 99 |
| The Monolithic View | p. 103 |
| Validation | p. 107 |
| Decomposition into Phones and Network | p. 108 |
| Refining the Network | p. 113 |
| Decomposing the Network | p. 119 |
| Integration | p. 128 |
| Implementation | p. 128 |
| Related Work | p. 129 |
| Conclusions | p. 129 |
| Developing a National Financial Information System | p. 131 |
| Introduction | p. 131 |
| Tax Information System | p. 133 |
| Prototype | p. 144 |
| Specifying a Distributed System | p. 146 |
| Conclusion | p. 152 |
| Multi-Lingual Document Processing | p. 155 |
| Introduction | p. 155 |
| Multi-Lingual Documents: Domain Analysis | p. 159 |
| The Formal Model of Multi-Lingual Documents | p. 168 |
| Operations for Editing Multi-Lingual Documents | p. 172 |
| Conclusions | p. 185 |
| Formalising Production Processes | p. 187 |
| Introduction | p. 187 |
| Modelling Products | p. 189 |
| Descriptive Production Modelling | p. 191 |
| Prescriptive Production Modelling | p. 209 |
| Relating Descriptive and Prescriptive Models | p. 210 |
| Conclusions | p. 215 |
| Model-Based Travel Planning | p. 219 |
| Introduction | p. 219 |
| Basic Concepts | p. 220 |
| Modelling for Travel Planning | p. 222 |
| Correctness: Relating Travel Plans | p. 230 |
| Development: Building Travel Plans | p. 231 |
| Model-Based Travel Assistant | p. 240 |
| Conclusions | p. 241 |
| Proving Safety of Authentication Protocols | p. 243 |
| Introduction | p. 243 |
| The Needham-Schroeder Protocol | p. 244 |
| Formalisation | p. 246 |
| The SSL Protocol | p. 253 |
| Principles | p. 256 |
| Related Work | p. 257 |
| Formalisation of Realm-Based Spatial Data Types | p. 259 |
| Introduction | p. 259 |
| Basic Types: Grid, Grid Point, and Grid Segment | p. 261 |
| Polygonal Lines and Segment Envelopes | p. 264 |
| Realms | p. 273 |
| Realm-Based Geometry | p. 276 |
| Conclusion | p. 285 |
| Object-Oriented Design Patterns | p. 287 |
| Introduction | p. 287 |
| A Formal Model of Object-Oriented Design | p. 288 |
| Linking Designs to Patterns | p. 301 |
| Specifying Properties of Patterns | p. 305 |
| Extending to Multiple Patterns | p. 310 |
| Conclusions | p. 313 |
| Automated Result Verification with AWK | p. 315 |
| Introduction | p. 315 |
| Modelling a Program | p. 317 |
| Program Execution Record | p. 319 |
| Result Verification | p. 322 |
| Result Specifications | p. 328 |
| Composition of Result Specifications | p. 331 |
| Specification-to-Verifier Generator | p. 334 |
| Application: WWW Access Log | p. 337 |
| Conclusions | p. 338 |
| Fail-Stop Components by Pattern Matching | p. 341 |
| Introduction | p. 341 |
| Components | p. 343 |
| Fault-Free versus Fail-Stop Components | p. 344 |
| Fail-Stop Components by Pattern Matching | p. 347 |
| Example: Line Editor | p. 353 |
| Specifying the Wrapper Generator | p. 355 |
| Implementing the Wrapper Generator | p. 365 |
| Conclusions | p. 367 |
| An Infrastructure for Software Reuse | p. 369 |
| Introduction | p. 369 |
| The Reuse Infrastructure | p. 370 |
| The Query System | p. 380 |
| Conclusions | p. 392 |
| About the Editors | p. 393 |
| About the Web Site | p. 395 |
| References | p. 397 |
| Table of Contents provided by Blackwell. All Rights Reserved. |
