Bowen Towards Verified Systems

1. Auflage 2013
ISBN: 978-1-4832-9152-9
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 2, 323 Seiten, Web PDF

Reihe: Real-Time Safety Critical Systems

As the complexity of embedded computer-controlled systems increases, the present industrial practice for their development gives cause for concern, especially for safety-critical applications where human lives are at stake. The use of software in such systems has increased enormously in the last decade. Formal methods, based on firm mathematical foundations, provide one means to help with reducing the risk of introducing errors during specification and development. There is currently much interest in both academic and industrial circles concerning the issues involved, but the techniques still need further investigation and promulgation to make their widespread use a reality.This book presents results of research into techniques to aid the formal verification of mixed hardware/software systems. Aspects of system specification and verification from requirements down to the underlying hardware are addressed, with particular regard to real-time issues. The work presented is largely based around the Occam programming language and Transputer microprocessor paradigm. The HOL theorem prover, based on higher order logic, has mainly been used in the application of machine-checked proofs.The book describes research work undertaken on the collaborative UK DTI/SERC-funded Information Engineering Dictorate Safemos project. The partners were Inmos Ltd., Cambridge SRI, the Oxford University Computing Laboratory and the University of Cambridge Computer Laboratory, who investigated the problems of formally verifying embedded systems. The most important results of the project are presented in the form of a series of interrelated chapters by project members and associated personnel. In addition, overviews of two other ventures with similar objectives are included as appendices.The material in this book is intended for computing science researchers and advanced industrial practitioners interested in the application of formal methods to real-time safety-critical systems at all levels of abstraction from requirements to hardware. In addition, material of a more general nature is presented, which may be of interest to managers in charge of projects applying formal methods, especially for safety-critical-systems, and others who are considering their use.

Autoren/Hrsg.

Bowen, J.

Inhaltsverzeichnis

1;Front Cover;1
2;Towards Verified Systems;4
3;Copyright Page;5
4;Table of Contents;6
5;List of Figures;14
6;List of Tables;16
7;Dedication;17
8;Foreword;18
9;Preface;20
10;Contact Addresses;24
11;Part I: Introduction;28
11.1;Chapter 1. Safety-Critical Systems and Formal Methods;30
11.1.1;1.1 A Brief Historical Perspective;30
11.1.2;1.2 Safety-critical Computer Systems;32
11.1.3;1.3 Industrial-scale Examples of Use;38
11.1.4;1.4 Areas of Application of Formal Methods;45
11.1.5;1.5 Safety Standards;49
11.1.6;1.6 Discussion;56
11.1.7;Acknowledgements;59
11.2;Chapter 2. Overview of the Project;62
11.2.1;2.1 The SAFEMOS Project;62
11.2.2;2.2 System Modelling;65
11.2.3;2.3 Software Development and Compilation;65
11.2.4;2.4 Hardware Design and Compilation;68
11.2.5;2.5 Other SAFEMOS Project Work;69
11.2.6;2.6 Related Work;73
11.2.7;2.7 Conclusion;73
12;Part II: Tools and Models;74
12.1;Chapter 3. The HOL Logic and System;76
12.1.1;3.1 Introduction;76
12.1.2;3.2 The HOL Logic;77
12.1.3;3.3 The HOL System;94
12.2;Chapter 4. Timed Transition Systems;98
12.2.1;4.1 Introduction to TTSs and HOL;98
12.2.2;4.2 Example: A Traffic Light Controller;100
12.2.3;4.3 A Real-Time Temporal Logic;102
12.2.4;4.4 Timed Transition Systems;105
12.2.5;4.5 Timed Transition Diagrams;107
12.2.6;4.6 Verification;110
12.2.7;4.7 Discussion;117
13;Part III: Software;118
13.1;Chapter 5. State Transition Assertions:
A Case Study;120
13.1.1;5.1 Introduction;120
13.1.2;5.2 An Example: Mult;121
13.1.3;5.3 A More Detailed Specification of Mult;124
13.1.4;5.4 Determining a Machine from a Program;124
13.1.5;5.5 State Transition Assertions;127
13.1.6;5.6 Formal Specification of Mult;130
13.1.7;5.7 Correctness of MultProg;131
13.1.8;5.8 Generating Atomic STAs;131
13.1.9;5.9 Laws for Combining STAs;134
13.1.10;5.10 Conclusions;139
13.2;Chapter 6. A Real-time Programming
Language;142
13.2.1;6.1 The SAFE Programming Language;142
13.2.2;6.2 Interval Model;144
13.2.3;6.3 Interval Semantics;146
13.2.4;6.4 SAFE Semantics;150
13.2.5;6.5 Laws;152
13.2.6;6.6 Conclusion;157
13.3;Chapter 7. Program Compilation;158
13.3.1;7.1 Machine Language Syntax;158
13.3.2;7.2 Machine Language Semantics;159
13.3.3;7.3 Compiler Specification;160
13.3.4;7.4 Correctness of Compilation;166
13.3.5;7.5 Proof of Correctness of Compilation;167
13.3.6;7.6 Conclusion;173
14;Part IV: Hardware;174
14.1;Chapter 8. A Framework for Microprocessor
Design;176
14.1.1;8.1 Introduction;176
14.1.2;8.2 Machine Specification Framework;180
14.1.3;8.3 Microcoded Machine Example;184
14.1.4;8.4 Incremental Model of Control Memory;188
14.1.5;8.5 Summary;192
14.2;Chapter 9. Designing a Processor;194
14.2.1;9.1 Instruction Set and Machine Architecture;194
14.2.2;9.2 Top Level Specification;197
14.2.3;9.3 Microcoded Implementation;204
14.2.4;9.4 Low-level Implementation;215
14.2.5;9.5 Conclusions;219
14.3;Chapter 10. Hardware Compilation;220
14.3.1;10.1 Introduction;220
14.3.2;10.2 A Language of Communicating Processes;223
14.3.3;10.3 Normal Form Implementation;226
14.3.4;10.4 Reduction to Normal Form;228
14.3.5;10.5 Example Proof;230
14.3.6;10.6 Rapid Prototype Compiler;232
14.3.7;10.7 Mapping Normal Form into Hardware;232
14.3.8;10.8 Conclusions;233
15;Part V: Technology Transfer;236
15.1;Chapter 11. Transfer into Industrial Design;238
15.1.1;11.1 Historical Background;238
15.1.2;11.2 Benefits from Formal Methods;240
15.1.3;11.3 Technology Transfer Problems;241
15.1.4;11.4 Requirements for Transfer of Formal Methods;244
15.1.5;11.5 Methods for Transferring Formal Methods;245
15.1.6;11.6 Technology Transfer from the SAFEMOS Project;247
16;Appendices: Related Work;250
16.1;Appendix A: System Verification and
the CLI Stack;252
16.1.1;A.1 Introduction;252
16.1.2;A.2 Our Philosophy of Systems Verification;254
16.1.3;A.3 Verifying Systems;255
16.1.4;A.4 The CLI Stack and Kit;261
16.1.5;A.5 Extending the Stack;272
16.1.6;A.6 Future Verified Systems;273
16.1.7;A.7 Conclusions;274
16.2;Appendix B: The ProCoS Project:
Provably Correct Systems;276
16.2.1;B.1 Introduction;276
16.2.2;B.2 History and Experience;279
16.2.3;B.3 Requirements Engineering and Duration Calculus;280
16.2.4;B.4 Program Specification and Development;285
16.2.5;B.5 Compiler Correctness;288
16.2.6;B.6 Base Systems;289
16.2.7;B.7 Conclusion;291
17;Acknowledgements;294
18;Bibliography;296