High-Integrity Software
Published on 1. July 2013
Book
Paperback/Softback
VIII, 360 pages
978-1-4684-5777-3 (ISBN)
Description
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.
More details
Series
Edition
Softcover reprint of the original 1st ed. 1989
Language
English
Place of publication
New York
United States
Target group
Professional and scholarly
Research
Illustrations
VIII, 360 p.
Dimensions
Height: 246 mm
Width: 189 mm
Thickness: 21 mm
Weight
719 gr
ISBN-13
978-1-4684-5777-3 (9781468457773)
DOI
10.1007/978-1-4684-5775-9
Schweitzer Classification
Other editions
Additional editions
C.T. Sennett
High-Integrity Software
Book
04/1990
Kluwer Academic / Plenum Publishers
€96.00
Article not available at the moment
Content
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.2Program 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.