High-Integrity Software

4. 3 The Gypsy language 72 4. 4 The Gypsy Verification Environment 73 4. 5 A simple example 81 4. 6 Specification data types 91 4. 7 Future directions 95 100 4. 8 Conclusions 5 Reliable programming in standard languages 102 Bernard Carre, Program Validation Ltd. 5. 1 Introduction 102 5. 2 Language requirements for high-integrity programming 103 5. 3 The use of standard languages 108 5. 4 Programming in Pascal and Ada 110 1'19 5. 5 Practical experiences NewSpeak: a reliable programming language 6 122 I. F. Currie, Royal Signals and Radar Establishment 6. 1 Introduction 122 6. 2 Types and values 127 6. 3 Declarations and variables 132 6. 4 Guarded declarations 134 6. 5 Cases and conditionals 136 6. 6 Loops 138 6. 7 Procedures 140 6. 8 Assertions 145 6. 9 Timing 147 6. 10 Conclusion 149 6. 11 Appendix 1: summary of syntax 150 6. 12 Appendix 2: type lattice and widening 156 7 Program analysis and systematic testing 159 M. A. Hennell, University of Liverpool, and D. Hedley and I. J. Riddell, Liverpool Data Research Associates Ltd. 7. 1 Introduction 159 7. 2 The basic requirement 160 7. 3 The Liverpool experience 161 7. 4 The Liverpool experiments 162 7. 5 The LDRA Testbeds 163 Interpretation 169 7. 6 7. 7 Applicability and benefits 171 7. 8 Safety-critical systems 173 VI 8 Program analysis and verification 176 Bernard Carre, Program Validation Ltd. 8. 1 Introduction 176 8.

Contenu

1 Introduction.- 2 Formal specification and implementation.- 2.1 Introduction to formal methods.- 2.2 Formal specification using Z.- 2.3 Formal implementation from Z.- 2.4 Conclusion.- 3 Designing for high integrity: The software fault tolerance approach.- 3.1 Introduction.- 3.2 Overview of software fault tolerance.- 3.3 Towards an implementation framework for software fault tolerance.- 3.4 Robust software using Ada's exception handling facilities.- 3.5 N-version programming.- 3.6 Recovery blocks.- 3.7 Comparison of N-version programming and recovery blocks.- 3.8 Practical application of N-version programming and recovery blocks.- 3.9 Summary.- 4 Practical experience with a formal verification system.- 4.1 Introduction.- 4.2 Background.- 4.3 The Gypsy language.- 4.4 The Gypsy Verification Environment.- 4.5 A simple example.- 4.6 Specification data types.- 4.7 Future directions.- 4.8 Conclusions.- 5 Reliable programming in standard languages.- 5.1 Introduction.- 5.2 Language requirements for high-integrity programming.- 5.3 The use of standard languages.- 5.4 Programming in Pascal and Ada.- 5.5 Practical experiences.- 6 NewSpeak: a reliable programming language.- 6.1 Introduction.- 6.2 Types and values.- 6.3 Declarations and variables.- 6.4 Guarded declarations.- 6.5 Cases and conditionals.- 6.6 Loops.- 6.7 Procedures.- 6.8 Assertions.- 6.9 Timing.- 6.10 Conclusion.- 6.11 Appendix 1: summary of syntax.- 6.12 Appendix 2: type lattice and widening.- 7 Program analysis and systematic testing.- 7.1 Introduction.- 7.2 The basic requirement.- 7.3 The Liverpool experience.- 7.4 The Liverpool experiments.- 7.5 The LDRA Testbeds.- 7.6 Interpretation.- 7.7 Applicability and benefits.- 7.8 Safety-critical systems.- 8 Program analysis and verification.- 8.1 Introduction.- 8.2 Program modelling.- 8.3 Flow analysis.- 8.4 Formal verification.- 8.5 Conclusions.- 9 The algebraic specification of a target machine: Ten15.- 9.1 Introduction.- 9.2 Types and operation.- 9.3 Features of the Ten15 machine.- 9.4 The formal method.- 9.5 Formal definition of Ten15.- 9.6 Conclusions.- 10 Assurance in high-integrity software.- 10.1 Introduction.- 10.2 Requirements and technical basis for assurance measures.- 10.3 Development.- 10.4 Requirements.- 10.5 Architecture.- 10.6 Evaluation.- 10.7 Configuration control.- 10.8 Complexity.- 10.9 Human computer interaction.- 10.10 Staff issues.- 10.11 Tools.- 10.12 Towards assurance measures.- 10.13 Conclusions.- 11 Modelling real-world issues for dependable software.- 11.1 Introduction.- 11.2 The importance of policies.- 11.3 Multiple levels of representation.- 11.4 Models for a communication system.- 11.5 Dependability breaches.- 11.6 Outline of the ATM system.- 11.7 Axegrinder rules.- 11.8 Views of the system.- 11.9 Composite view of the system.- 11.10 Behavioural model of the system.- 11.11 Vulnerability analysis.- 11.12 Analysis of communication.- 11.13 Analysis of system conformation.- 11.14 Message analysis.- 11.15 Behavioural analysis.- 11.16 What enforces the rules?.- 11.17 Final summary: The analytical method in outline.- 12 Contractual specification of reliable software.- 12.1 The procurement process for high-integrity software.- 12.2 Procurement issues at the feasibility study stage.- 12.3 High-integrity considerations during project definition.- 12.4 The development environment for trusted software.- 12.5 The formal specification of access control policies.