| Preface | p. xi |
| General Applications of Formal Methods and Systems | |
| Designware: Software Development by Refinement | p. 3 |
| Overview | p. 3 |
| Basic Concepts | p. 4 |
| Specifications | p. 4 |
| Morphisms | p. 6 |
| The Category of Specs | p. 8 |
| Diagrams | p. 9 |
| The Structuring of Specifications | p. 10 |
| Refinement and Diagrams | p. 11 |
| Logic Morphisms and Code Generation | p. 12 |
| Software Development by Refinement | p. 12 |
| Constructing Specifications | p. 13 |
| Constructing Refinements | p. 13 |
| Scaling up | p. 15 |
| Design by Classification: Taxonomies of Refinements | p. 15 |
| Tactics | p. 18 |
| Summary | p. 20 |
| B: Towards Zero Defect Software | p. 23 |
| B and Mathematical Methods | p. 23 |
| B and the Software Process | p. 24 |
| The Method and the Tools | p. 25 |
| Abstract Machines | p. 27 |
| Generalised Substitutions | p. 29 |
| Structuring Specifications | p. 31 |
| Including Machines | p. 31 |
| Sharing Machines | p. 32 |
| Machine Refinement | p. 32 |
| Machine Implementation | p. 34 |
| Structuring Designs | p. 35 |
| The IMPORTS and SEES Clauses | p. 36 |
| The B-Toolkit Components | p. 36 |
| The B-Toolkit Managers | p. 36 |
| Analysis | p. 37 |
| Animation | p. 37 |
| Proof | p. 38 |
| Specification/Module Library | p. 38 |
| Code Generation | p. 39 |
| Base Generators | p. 39 |
| Documentation | p. 40 |
| History of B | p. 40 |
| Conclusion | p. 40 |
| The Use of B to Specify, Design and Verify Hardware | p. 43 |
| Introduction | p. 43 |
| The useful limit of formal methods in hardware development | p. 45 |
| Justification for the use of the B-Toolkit and VHDL | p. 45 |
| Overview of B | p. 46 |
| Overview of VHDL | p. 46 |
| Abstract specification | p. 47 |
| Refinement | p. 49 |
| Detailed refinement | p. 49 |
| Data refinement | p. 50 |
| Structural refinement | p. 51 |
| AMN to VHDL translation | p. 56 |
| Hardware animation | p. 59 |
| Future work | p. 60 |
| Conclusions | p. 61 |
| Acknowledgments | p. 61 |
| A System for Predictable Component-Based Software Construction | p. 63 |
| Introduction | p. 64 |
| Formal Specification of an Optimization Problem | p. 66 |
| An Amortized Cost Realization | p. 72 |
| Discussion | p. 80 |
| Acknowledgments | p. 81 |
| Autonomous Decentralized Systems | p. 89 |
| Introduction | p. 89 |
| Background of the Tokyo Metropolitan-Area Railway System | p. 91 |
| System Requirements | p. 92 |
| Autonomous Decentralized Systems | p. 93 |
| ADS Concept | p. 94 |
| ADS Architecture | p. 95 |
| The Data Field | p. 95 |
| Data-Driven Mechanism | p. 97 |
| ADS Technologies | p. 97 |
| Fault-Tolerance | p. 97 |
| On-Line Expansion | p. 99 |
| On-Line Maintenance | p. 100 |
| Assurance | p. 101 |
| Autonomous Decentralized Transport Operation Control System -ATOS | p. 105 |
| System Structure | p. 106 |
| Conclusions | p. 109 |
| Case Study | |
| Bay Area Rapid Transit System Case Study | p. 115 |
| Objective | p. 115 |
| General Background on the BART Train System | p. 116 |
| Informal Specification for the AATC System | p. 118 |
| Inputs and Outputs to the Control Algorithm | p. 121 |
| Physical Performance of the Train in Response to Commands | p. 122 |
| Worst Case Stopping Profile | p. 124 |
| Considerations with Acceleration and Speed Commands | p. 129 |
| Quantitative Quality and Safety Metrics to be Demonstrated | p. 130 |
| Vital Station Computer (VSC) Issues | p. 132 |
| Miscellaneous Questions and Answers | p. 132 |
| Using SCR to Specify the BART Requirements | p. 137 |
| Introduction | p. 137 |
| SCR Method | p. 139 |
| SCR Notation and Tables | p. 140 |
| SCR* Toolset | p. 140 |
| Applying SCR to Practical Systems | p. 141 |
| Managing Complexity | p. 141 |
| Specifying the AATC System Requirements | p. 143 |
| System Properties | p. 144 |
| System Requirements | p. 145 |
| Monitored and Controlled Variables | p. 146 |
| Constants, User-Defined Types, and Terms | p. 149 |
| Defining the System Modes | p. 151 |
| Defining the Ideal System Behavior | p. 153 |
| System Design | p. 158 |
| Software Requirements | p. 159 |
| Applying the SCR Tools | p. 160 |
| Discussion | p. 162 |
| Benefits | p. 162 |
| Some Issues | p. 163 |
| Conclusion | p. 165 |
| A Domain Language for a Class of Reactive Systems | p. 169 |
| Overview | p. 169 |
| A Model of Reactive Systems | p. 170 |
| Domain Specific Predictive Models | p. 174 |
| Partitioning of the State Space | p. 176 |
| Basic Safety | p. 177 |
| Discrete Profiles | p. 180 |
| Describing BART in Terms of Profiles | p. 180 |
| Stopping Profiles | p. 181 |
| Discrete and Continuous Profiles | p. 182 |
| Using Profiles to Model Constraints | p. 183 |
| A Refined View of Safety | p. 184 |
| The Domain Language | p. 185 |
| Problem Specific Information | p. 186 |
| Foundation | p. 186 |
| Reasoning Support | p. 188 |
| RRL | p. 188 |
| The Specification of BART | p. 191 |
| Conclusions and Future Work | p. 195 |
| Refinement-based Derivation of Train Controllers | p. 197 |
| Transformation and High Integrity Software Development | p. 198 |
| Verification | p. 199 |
| Background | p. 200 |
| Transformation | p. 201 |
| Distinctions between Rewriting and Transformation | p. 202 |
| Formal Transformation | p. 203 |
| An Overview of HATS | p. 203 |
| Applications | p. 204 |
| The Specification of BART | p. 205 |
| An Overview of a Domain Language | p. 206 |
| An Algorithmic Specification of a Simplified Controller for BART | p. 207 |
| Transforming the Bart Specification | p. 212 |
| Optimization | p. 215 |
| An Optimization Example | p. 215 |
| Proving Optimizations Correct using RRL | p. 216 |
| RRL | p. 217 |
| Illustration: Proving correctness of an Optimization | p. 220 |
| Some Optimizations | p. 221 |
| Execution Results | p. 225 |
| Conclusions and Future Work | p. 226 |
| Verification and Validation | |
| Validation of a Relational Program | p. 243 |
| Introduction | p. 244 |
| System Model | p. 246 |
| Specification of the BART Control Program | p. 248 |
| Overview | p. 248 |
| Problem Modification | p. 250 |
| Transformational Development | p. 250 |
| Requirements Decomposition | p. 253 |
| Safety-Stop | p. 254 |
| Safety-Speed | p. 256 |
| Reach Destination or Time Optimization | p. 256 |
| Smoothness | p. 256 |
| Implementation | p. 256 |
| Simulator | p. 257 |
| Safety-stop | p. 258 |
| Safety-Velocity | p. 259 |
| Reach -Destination | p. 259 |
| Summary | p. 263 |
| Acknowledgment | p. 263 |
| Verification of a Controller for BART | p. 265 |
| Introduction | p. 266 |
| Semantics-based Verification | p. 267 |
| Denotational Semantics | p. 267 |
| Logic Programming | p. 268 |
| Partial Evaluation | p. 269 |
| Horn Logic Denotational Semantics | p. 270 |
| An Example of Logical Denotational Semantics | p. 271 |
| The BART System | p. 276 |
| Description of the BART system | p. 277 |
| Advanced Automatic Train Control (AATC) | p. 277 |
| Operating environment of the station controllers | p. 278 |
| Overall design of the station controller | p. 279 |
| Worst-case stopping profile | p. 279 |
| Ada Implementation of BART Controller | p. 280 |
| Design of the NVSC | p. 282 |
| Real-time properties of the Controller | p. 283 |
| Verification of the Ada Implementation | p. 284 |
| Horn Logical Denotational Semantics of Ada | p. 286 |
| Partially Evaluating the Denotation | p. 286 |
| Abstract Verification of the Controller | p. 287 |
| Advantages of our Approach | p. 289 |
| Verifying the Timing Properties | p. 290 |
| Conclusion and Related Work | p. 290 |
| Using Virtual Reality to Validate System Models | p. 301 |
| Background | p. 301 |
| The Role of Validation in High Consequence System Development | p. 303 |
| Models: Mental, Virtual, and Formal | p. 304 |
| Graphical Representations of Formal Models | p. 305 |
| Display Issues | p. 308 |
| Displaying Predicates | p. 309 |
| The Flatland Virtual Environment Shell | p. 311 |
| Example: A Robotic System | p. 312 |
| Conclusions and Future Work | p. 319 |
| Acknowledgements | p. 319 |
| Index | p. 321 |
| Table of Contents provided by Syndetics. All Rights Reserved. |