Item Details

Print View

High Integrity Software

edited by Victor L. Winter, Sourav Bhattacharya
Format
Book
Published
Boston, MA : Kluwer Academic Publishers, 2001.
Language
English
Series
Kluwer International Series in Engineering and Computer Science
ISBN
0792379497 (alk. paper)
Contents
  • Part I General Applications of Formal Methods and Systems
  • 1 Designware: Software Development by Refinement / Douglas R. Smith 3
  • 1.2.1 Specifications 4
  • 1.2.2 Morphisms 6
  • 1.2.3 Category of Specs 8
  • 1.2.4 Diagrams 9
  • Structuring of Specifications 10
  • Refinement and Diagrams 11
  • 1.2.5 Logic Morphisms and Code Generation 12
  • 1.3 Software Development by Refinement 12
  • 1.3.1 Constructing Specifications 13
  • 1.3.2 Constructing Refinements 13
  • 1.4 Scaling up 15
  • 1.4.1 Design by Classification: Taxonomies of Refinements 15
  • 1.4.2 Tactics 18
  • 2 B: Towards Zero Defect Software / Ib Sorensen, David Neilson 23
  • 2.1 B and Mathematical Methods 23
  • 2.2 B and the Software Process 24
  • 2.3 Method and the Tools 25
  • 2.4 Abstract Machines 27
  • 2.4.1 Generalised Substitutions 29
  • 2.4.2 Structuring Specifications 31
  • Including Machines 31
  • Sharing Machines 32
  • 2.5 Machine Refinement 32
  • 2.6 Machine Implementation 34
  • 2.6.1 Structuring Designs 35
  • IMPORTS and SEES Clauses 36
  • 2.7 B-Toolkit Components 36
  • 2.7.1 B-Toolkit Managers 36
  • 2.7.2 Analysis 37
  • 2.7.3 Animation 37
  • 2.7.4 Proof 38
  • 2.7.5 Specification/Module Library 38
  • 2.7.6 Code Generation 39
  • 2.7.7 Base Generators 39
  • 2.7.8 Documentation 40
  • 2.8 History of B 40
  • 3 Use of B to Specify, Design and Verify Hardware / Wilson Ifill, Ib Sorensen, Steve Schneider 43
  • 3.1.1 Useful limit of formal methods in hardware development 45
  • 3.1.2 Justification for the use of the B-Toolkit and VHDL 45
  • 3.1.3 Overview of B 46
  • 3.1.4 Overview of VHDL 46
  • 3.2 Abstract specification 47
  • 3.3 Refinement 49
  • 3.3.1 Detailed refinement 49
  • 3.3.2 Data refinement 50
  • 3.3.3 Structural refinement 51
  • 3.4 AMN to VHDL translation 56
  • 3.5 Hardware animation 59
  • 3.6 Future work 60
  • 4 A System for Predictable Component-Based Software Construction / M. Aronszajn, M. Sitaraman, S. Atkinson, G. Kulczycki 63
  • 4.2 Formal Specification of an Optimization Problem 66
  • 4.3 An Amortized Cost Realization 72
  • 5 Autonomous Decentralized Systems / Kinji Mori 89
  • 5.2 Background of the Tokyo Metropolitan-Area Railway System 91
  • 5.3 System Requirements 92
  • 5.4 Autonomous Decentralized Systems 93
  • 5.4.1 ADS Concept 94
  • 5.4.2 ADS Architecture 95
  • Data Field 95
  • Data-Driven Mechanism 97
  • 5.4.3 ADS Technologies 97
  • Fault-Tolerance 97
  • On-Line Expansion 99
  • On-Line Maintenance 100
  • Assurance 101
  • 5.5 Autonomous Decentralized Transport Operation Control System -ATOS 105
  • 5.5.1 System Structure 106
  • 6 Bay Area Rapid Transit System Case Study / Victor L. Winter, Raymond S. Berg, James T. Ringland 115
  • 6.2 General Background on the BART Train System 116
  • 6.3 Informal Specification for the AATC System 118
  • 6.4 Inputs and Outputs to the Control Algorithm 121
  • 6.5 Physical Performance of the Train in Response to Commands 122
  • 6.6 Worst Case Stopping Profile 124
  • 6.7 Considerations with Acceleration and Speed Commands 129
  • 6.8 Quantitative Quality and Safety Metrics to be Demonstrated 130
  • 6.9 Vital Station Computer (VSC) Issues 132
  • 6.10 Miscellaneous Questions and Answers 132
  • 7 Using SCR to Specify the BART Requirements / Constance Heitmeyer 137
  • 7.2 SCR Method 139
  • SCR Notation and Tables 140
  • SCR* Toolset 140
  • Applying SCR to Practical Systems 141
  • 7.3 Managing Complexity 141
  • 7.4 Specifying the AATC System Requirements 143
  • 7.4.1 System Properties 144
  • 7.4.2 System Requirements 145
  • Monitored and Controlled Variables 146
  • Constants, User-Defined Types, and Terms 149
  • Defining the System Modes 151
  • Defining the Ideal System Behavior 153
  • 7.4.3 System Design 158
  • 7.4.4 Software Requirements 159
  • 7.5t Applying the SCR Tools 160
  • 7.6.1 Benefits 162
  • 8 A Domain Language for a Class of Reactive Systems / Deepak Kapur, Victor L. Winter 169
  • 8.2 A Model of Reactive Systems 170
  • 8.3 Domain Specific Predictive Models 174
  • 8.3.1 Partitioning of the State Space 176
  • Basic Safety 177
  • 8.4 Discrete Profiles 180
  • 8.4.1 Describing BART in Terms of Profiles 180
  • Stopping Profiles 181
  • 8.4.2 Discrete and Continuous Profiles 182
  • 8.5 Using Profiles to Model Constraints 183
  • 8.5.1 A Refined View of Safety 184
  • 8.6 Domain Language 185
  • 8.6.1 Problem Specific Information 186
  • 8.6.2 Foundation 186
  • 8.7 Reasoning Support 188
  • 8.7.1 RRL 188
  • 8.8 Specification of BART 191
  • 8.9 Conclusions and Future Work 195
  • 9 Refinement-based Derivation of Train Controllers / Victor L. Winter, Deepak Kapur, Raymond S. Berg 197
  • 9.1 Transformation and High Integrity Software Development 198
  • 9.1.1 Verification 199
  • 9.2.1 Transformation 201
  • Distinctions between Rewriting and Transformation 202
  • 9.2.2 Formal Transformation 203
  • 9.3 An Overview of HATS 203
  • 9.3.1 Applications 204
  • 9.4 Specification of BART 205
  • 9.4.1 An Overview of a Domain Language 206
  • 9.4.2 An Algorithmic Specification of a Simplified Controller for BART 207
  • 9.5 Transforming the Bart Specification 212
  • 9.5.1 Optimization 215
  • 9.5.2 An Optimization Example 215
  • 9.6 Proving Optimizations Correct using RRL 216
  • 9.6.1 RRL 217
  • 9.6.2 Illustration: Proving correctness of an Optimization 220
  • 9.7 Some Optimizations 221
  • 9.8 Execution Results 225
  • 9.9 Conclusions and Future Work 226
  • Part III Verification and Validation
  • 10 Validation of a Relational Program / F. B. Bastani, V. Reddy, P. Srigiriraju, I.-L. Yen 243
  • 10.2 System Model 246
  • 10.3 Specification of the BART Control Program 248
  • 10.3.2 Problem Modification 250
  • 10.3.3 Transformational Development 250
  • 10.4 Requirements Decomposition 253
  • 10.4.1 Safety-Stop 254
  • 10.4.2 Safety-Speed 256
  • 10.4.3 Reach Destination or Time Optimization 256
  • 10.4.4 Smoothness 256
  • 10.5 Implementation 256
  • 10.5.1 Simulator 257
  • 10.5.2 Safety-stop 258
  • 10.5.3 Safety-Velocity 259
  • 10.5.4 Reach -Destination 259
  • 11 Verification of a Controller for BART / Lawrence King, Gopal Gupta, Enrico Pontelli 265
  • 11.2 Semantics-based Verification 267
  • 11.2.1 Denotational Semantics 267
  • 11.2.2 Logic Programming 268
  • 11.2.3 Partial Evaluation 269
  • 11.2.4 Horn Logic Denotational Semantics 270
  • 11.2.5 An Example of Logical Denotational Semantics 271
  • 11.3 BART System 276
  • 11.3.1 Description of the BART system 277
  • 11.3.2 Advanced Automatic Train Control (AATC) 277
  • 11.3.3 Operating environment of the station controllers 278
  • 11.3.4 Overall design of the station controller 279
  • 11.3.5 Worst-case stopping profile 279
  • 11.3.6 Ada Implementation of BART Controller 280
  • 11.3.7 Design of the NVSC 282
  • 11.3.8 Real-time properties of the Controller 283
  • 11.4 Verification of the Ada Implementation 284
  • 11.4.1 Horn Logical Denotational Semantics of Ada 286
  • 11.4.2 Partially Evaluating the Denotation 286
  • 11.4.3 Abstract Verification of the Controller 287
  • 11.4.4 Advantages of our Approach 289
  • 11.5 Verifying the Timing Properties 290
  • 12 Using Virtual Reality to Validate System Models / Victor L. Winter, Thomas P. Caudell 301
  • 12.2 Role of Validation in High Consequence System Development 303
  • 12.3 Models: Mental, Virtual, and Formal 304
  • 12.4 Graphical Representations of Formal Models 305
  • 12.4.1 Display Issues 308
  • Displaying Predicates 309
  • 12.5 Flatland Virtual Environment Shell 311
  • 12.6 Example: A Robotic System 312
  • 12.7 Conclusions and Future Work 319.
Description
xiv, 320 p. : ill. ; 24 cm.
Notes
Includes bibliographical references and index.
Series Statement
Kluwer international series in engineering and computer science SECS 577
Technical Details
  • Access in Virgo Classic
  • Staff View

    LEADER 09115cam a22003494a 4500
    001 u3733219
    003 SIRSI
    005 20010606110318.0
    008 010302s2001 maua b 001 0 eng
    010
      
      
    a| 2001022474
    020
      
      
    a| 0792379497 (alk. paper)
    035
      
      
    a| (Sirsi) i0792379497
    035
      
      
    a| (OCoLC)46394537
    040
      
      
    a| DLC c| DLC d| DLC d| MvI
    042
      
      
    a| pcc
    050
    0
    0
    a| QA76.76.R44 b| H54 2001
    082
    0
    0
    a| 005 2| 21
    090
      
      
    a| SCIENG/QA76.76.R44 b| H54 2001
    245
    0
    0
    a| High integrity software / c| edited by Victor L. Winter, Sourav Bhattacharya.
    260
      
      
    a| Boston, MA : b| Kluwer Academic Publishers, c| 2001.
    300
      
      
    a| xiv, 320 p. : b| ill. ; c| 24 cm.
    440
      
    0
    a| Kluwer international series in engineering and computer science v| SECS 577
    504
      
      
    a| Includes bibliographical references and index.
    505
    0
    0
    g| Part I t| General Applications of Formal Methods and Systems -- g| 1 t| Designware: Software Development by Refinement / r| Douglas R. Smith g| 3 -- g| 1.2.1 t| Specifications g| 4 -- g| 1.2.2 t| Morphisms g| 6 -- g| 1.2.3 t| Category of Specs g| 8 -- g| 1.2.4 t| Diagrams g| 9 -- t| Structuring of Specifications g| 10 -- t| Refinement and Diagrams g| 11 -- g| 1.2.5 t| Logic Morphisms and Code Generation g| 12 -- g| 1.3 t| Software Development by Refinement g| 12 -- g| 1.3.1 t| Constructing Specifications g| 13 -- g| 1.3.2 t| Constructing Refinements g| 13 -- g| 1.4 t| Scaling up g| 15 -- g| 1.4.1 t| Design by Classification: Taxonomies of Refinements g| 15 -- g| 1.4.2 t| Tactics g| 18 -- g| 2 t| B: Towards Zero Defect Software / r| Ib Sorensen, David Neilson g| 23 -- g| 2.1 t| B and Mathematical Methods g| 23 -- g| 2.2 t| B and the Software Process g| 24 -- g| 2.3 t| Method and the Tools g| 25 -- g| 2.4 t| Abstract Machines g| 27 -- g| 2.4.1 t| Generalised Substitutions g| 29 -- g| 2.4.2 t| Structuring Specifications g| 31 -- t| Including Machines g| 31 -- t| Sharing Machines g| 32 -- g| 2.5 t| Machine Refinement g| 32 -- g| 2.6 t| Machine Implementation g| 34 -- g| 2.6.1 t| Structuring Designs g| 35 -- t| IMPORTS and SEES Clauses g| 36 -- g| 2.7 t| B-Toolkit Components g| 36 -- g| 2.7.1 t| B-Toolkit Managers g| 36 -- g| 2.7.2 t| Analysis g| 37 -- g| 2.7.3 t| Animation g| 37 -- g| 2.7.4 t| Proof g| 38 -- g| 2.7.5 t| Specification/Module Library g| 38 -- g| 2.7.6 t| Code Generation g| 39 -- g| 2.7.7 t| Base Generators g| 39 -- g| 2.7.8 t| Documentation g| 40 -- g| 2.8 t| History of B g| 40 -- g| 3 t| Use of B to Specify, Design and Verify Hardware / r| Wilson Ifill, Ib Sorensen, Steve Schneider g| 43 -- g| 3.1.1 t| Useful limit of formal methods in hardware development g| 45 -- g| 3.1.2 t| Justification for the use of the B-Toolkit and VHDL g| 45 -- g| 3.1.3 t| Overview of B g| 46 -- g| 3.1.4 t| Overview of VHDL g| 46 -- g| 3.2 t| Abstract specification g| 47 -- g| 3.3 t| Refinement g| 49 -- g| 3.3.1 t| Detailed refinement g| 49 -- g| 3.3.2 t| Data refinement g| 50 -- g| 3.3.3 t| Structural refinement g| 51 -- g| 3.4 t| AMN to VHDL translation g| 56 -- g| 3.5 t| Hardware animation g| 59 -- g| 3.6 t| Future work g| 60 -- g| 4 t| A System for Predictable Component-Based Software Construction / r| M. Aronszajn, M. Sitaraman, S. Atkinson, G. Kulczycki g| 63 -- g| 4.2 t| Formal Specification of an Optimization Problem g| 66 -- g| 4.3 t| An Amortized Cost Realization g| 72 -- g| 5 t| Autonomous Decentralized Systems / r| Kinji Mori g| 89 -- g| 5.2 t| Background of the Tokyo Metropolitan-Area Railway System g| 91 -- g| 5.3 t| System Requirements g| 92 -- g| 5.4 t| Autonomous Decentralized Systems g| 93 -- g| 5.4.1 t| ADS Concept g| 94 -- g| 5.4.2 t| ADS Architecture g| 95 -- t| Data Field g| 95 -- t| Data-Driven Mechanism g| 97 -- g| 5.4.3 t| ADS Technologies g| 97 -- t| Fault-Tolerance g| 97 -- t| On-Line Expansion g| 99 -- t| On-Line Maintenance g| 100 -- t| Assurance g| 101 -- g| 5.5 t| Autonomous Decentralized Transport Operation Control System -ATOS g| 105 -- g| 5.5.1 t| System Structure g| 106 -- g| 6 t| Bay Area Rapid Transit System Case Study / r| Victor L. Winter, Raymond S. Berg, James T. Ringland g| 115 -- g| 6.2 t| General Background on the BART Train System g| 116 -- g| 6.3 t| Informal Specification for the AATC System g| 118 -- g| 6.4 t| Inputs and Outputs to the Control Algorithm g| 121 -- g| 6.5 t| Physical Performance of the Train in Response to Commands g| 122 -- g| 6.6 t| Worst Case Stopping Profile g| 124 -- g| 6.7 t| Considerations with Acceleration and Speed Commands g| 129 -- g| 6.8 t| Quantitative Quality and Safety Metrics to be Demonstrated g| 130 -- g| 6.9 t| Vital Station Computer (VSC) Issues g| 132 -- g| 6.10 t| Miscellaneous Questions and Answers g| 132 -- g| 7 t| Using SCR to Specify the BART Requirements / r| Constance Heitmeyer g| 137 -- g| 7.2 t| SCR Method g| 139 -- t| SCR Notation and Tables g| 140 -- t| SCR* Toolset g| 140 -- t| Applying SCR to Practical Systems g| 141 -- g| 7.3 t| Managing Complexity g| 141 -- g| 7.4 t| Specifying the AATC System Requirements g| 143 -- g| 7.4.1 t| System Properties g| 144 -- g| 7.4.2 t| System Requirements g| 145 -- t| Monitored and Controlled Variables g| 146 -- t| Constants, User-Defined Types, and Terms g| 149 -- t| Defining the System Modes g| 151 -- t| Defining the Ideal System Behavior g| 153 -- g| 7.4.3 t| System Design g| 158 -- g| 7.4.4 t| Software Requirements g| 159 -- g| 7.5t t| Applying the SCR Tools g| 160 -- g| 7.6.1 t| Benefits g| 162 -- g| 8 t| A Domain Language for a Class of Reactive Systems / r| Deepak Kapur, Victor L. Winter g| 169 -- g| 8.2 t| A Model of Reactive Systems g| 170 -- g| 8.3 t| Domain Specific Predictive Models g| 174 -- g| 8.3.1 t| Partitioning of the State Space g| 176 -- t| Basic Safety g| 177 -- g| 8.4 t| Discrete Profiles g| 180 -- g| 8.4.1 t| Describing BART in Terms of Profiles g| 180 -- t| Stopping Profiles g| 181 -- g| 8.4.2 t| Discrete and Continuous Profiles g| 182 -- g| 8.5 t| Using Profiles to Model Constraints g| 183 -- g| 8.5.1 t| A Refined View of Safety g| 184 -- g| 8.6 t| Domain Language g| 185 -- g| 8.6.1 t| Problem Specific Information g| 186 -- g| 8.6.2 t| Foundation g| 186 -- g| 8.7 t| Reasoning Support g| 188 -- g| 8.7.1 t| RRL g| 188 -- g| 8.8 t| Specification of BART g| 191 -- g| 8.9 t| Conclusions and Future Work g| 195 -- g| 9 t| Refinement-based Derivation of Train Controllers / r| Victor L. Winter, Deepak Kapur, Raymond S. Berg g| 197 -- g| 9.1 t| Transformation and High Integrity Software Development g| 198 -- g| 9.1.1 t| Verification g| 199 -- g| 9.2.1 t| Transformation g| 201 -- t| Distinctions between Rewriting and Transformation g| 202 -- g| 9.2.2 t| Formal Transformation g| 203 -- g| 9.3 t| An Overview of HATS g| 203 -- g| 9.3.1 t| Applications g| 204 -- g| 9.4 t| Specification of BART g| 205 -- g| 9.4.1 t| An Overview of a Domain Language g| 206 -- g| 9.4.2 t| An Algorithmic Specification of a Simplified Controller for BART g| 207 -- g| 9.5 t| Transforming the Bart Specification g| 212 -- g| 9.5.1 t| Optimization g| 215 -- g| 9.5.2 t| An Optimization Example g| 215 -- g| 9.6 t| Proving Optimizations Correct using RRL g| 216 -- g| 9.6.1 t| RRL g| 217 -- g| 9.6.2 t| Illustration: Proving correctness of an Optimization g| 220 -- g| 9.7 t| Some Optimizations g| 221 -- g| 9.8 t| Execution Results g| 225 -- g| 9.9 t| Conclusions and Future Work g| 226 -- g| Part III t| Verification and Validation -- g| 10 t| Validation of a Relational Program / r| F. B. Bastani, V. Reddy, P. Srigiriraju, I.-L. Yen g| 243 -- g| 10.2 t| System Model g| 246 -- g| 10.3 t| Specification of the BART Control Program g| 248 -- g| 10.3.2 t| Problem Modification g| 250 -- g| 10.3.3 t| Transformational Development g| 250 -- g| 10.4 t| Requirements Decomposition g| 253 -- g| 10.4.1 t| Safety-Stop g| 254 -- g| 10.4.2 t| Safety-Speed g| 256 -- g| 10.4.3 t| Reach Destination or Time Optimization g| 256 -- g| 10.4.4 t| Smoothness g| 256 -- g| 10.5 t| Implementation g| 256 -- g| 10.5.1 t| Simulator g| 257 -- g| 10.5.2 t| Safety-stop g| 258 -- g| 10.5.3 t| Safety-Velocity g| 259 -- g| 10.5.4 t| Reach -Destination g| 259 -- g| 11 t| Verification of a Controller for BART / r| Lawrence King, Gopal Gupta, Enrico Pontelli g| 265 -- g| 11.2 t| Semantics-based Verification g| 267 -- g| 11.2.1 t| Denotational Semantics g| 267 -- g| 11.2.2 t| Logic Programming g| 268 -- g| 11.2.3 t| Partial Evaluation g| 269 -- g| 11.2.4 t| Horn Logic Denotational Semantics g| 270 -- g| 11.2.5 t| An Example of Logical Denotational Semantics g| 271 -- g| 11.3 t| BART System g| 276 -- g| 11.3.1 t| Description of the BART system g| 277 -- g| 11.3.2 t| Advanced Automatic Train Control (AATC) g| 277 -- g| 11.3.3 t| Operating environment of the station controllers g| 278 -- g| 11.3.4 t| Overall design of the station controller g| 279 -- g| 11.3.5 t| Worst-case stopping profile g| 279 -- g| 11.3.6 t| Ada Implementation of BART Controller g| 280 -- g| 11.3.7 t| Design of the NVSC g| 282 -- g| 11.3.8 t| Real-time properties of the Controller g| 283 -- g| 11.4 t| Verification of the Ada Implementation g| 284 -- g| 11.4.1 t| Horn Logical Denotational Semantics of Ada g| 286 -- g| 11.4.2 t| Partially Evaluating the Denotation g| 286 -- g| 11.4.3 t| Abstract Verification of the Controller g| 287 -- g| 11.4.4 t| Advantages of our Approach g| 289 -- g| 11.5 t| Verifying the Timing Properties g| 290 -- g| 12 t| Using Virtual Reality to Validate System Models / r| Victor L. Winter, Thomas P. Caudell g| 301 -- g| 12.2 t| Role of Validation in High Consequence System Development g| 303 -- g| 12.3 t| Models: Mental, Virtual, and Formal g| 304 -- g| 12.4 t| Graphical Representations of Formal Models g| 305 -- g| 12.4.1 t| Display Issues g| 308 -- t| Displaying Predicates g| 309 -- g| 12.5 t| Flatland Virtual Environment Shell g| 311 -- g| 12.6 t| Example: A Robotic System g| 312 -- g| 12.7 t| Conclusions and Future Work g| 319.
    596
      
      
    a| 5
    650
      
    0
    a| Computer software x| Reliability.
    650
      
    0
    a| Computer software x| Development.
    700
    1
      
    a| Winter, Victor L.
    700
    1
      
    a| Bhattacharya, Sourav.
    999
      
      
    a| QA76.76 .R44 H54 2001 w| LC i| X004523585 l| STACKS m| SCI-ENG t| BOOK
▾See more
▴See less

Availability

Google Preview

Google Books Preview
Library Location Map Availability Call Number
Brown Science and Engineering Stacks N/A Available