Towards Verified Systems (eBook)

J. Bowen (Herausgeber)

eBook Download: PDF

2013 | 1. Auflage
323 Seiten
Elsevier Science (Verlag)
978-1-4832-9152-9 (ISBN)

Infos

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.

Inhalt

Front Cover 1
Towards Verified Systems 4
Copyright Page 5
Table of Contents 6
List of Figures 14
List of Tables 16
Dedication 17
Foreword 18
Preface 20
Contact Addresses 24
Part I: Introduction 28
Chapter 1. Safety-Critical Systems and Formal Methods 30
1.1 A Brief Historical Perspective 30
1.2 Safety-critical Computer Systems 32
1.3 Industrial-scale Examples of Use 38
1.4 Areas of Application of Formal Methods 45
1.5 Safety Standards 49
1.6 Discussion 56
Acknowledgements 59
Chapter 2. Overview of the Project 62
2.1 The SAFEMOS Project 62
2.2 System Modelling 65
2.3 Software Development and Compilation 65
2.4 Hardware Design and Compilation 68
2.5 Other SAFEMOS Project Work 69
2.6 Related Work 73
2.7 Conclusion 73
Part II: Tools and Models 74
Chapter 3. The HOL Logic and System 76
3.1 Introduction 76
3.2 The HOL Logic 77
3.3 The HOL System 94
Chapter 4. Timed Transition Systems 98
4.1 Introduction to TTSs and HOL 98
4.2 Example: A Traffic Light Controller 100
4.3 A Real-Time Temporal Logic 102
4.4 Timed Transition Systems 105
4.5 Timed Transition Diagrams 107
4.6 Verification 110
4.7 Discussion 117
Part III: Software 118
Chapter 5. State Transition Assertions: 
120 
5.1 Introduction 120
5.2 An Example: Mult 121
5.3 A More Detailed Specification of Mult 124
5.4 Determining a Machine from a Program 124
5.5 State Transition Assertions 127
5.6 Formal Specification of Mult 130
5.7 Correctness of MultProg 131
5.8 Generating Atomic STAs 131
5.9 Laws for Combining STAs 134
5.10 Conclusions 139
Chapter 6. A Real-time Programming 
142 
6.1 The SAFE Programming Language 142
6.2 Interval Model 144
6.3 Interval Semantics 146
6.4 SAFE Semantics 150
6.5 Laws 152
6.6 Conclusion 157
Chapter 7. Program Compilation 158
7.1 Machine Language Syntax 158
7.2 Machine Language Semantics 159
7.3 Compiler Specification 160
7.4 Correctness of Compilation 166
7.5 Proof of Correctness of Compilation 167
7.6 Conclusion 173
Part IV: Hardware 174
Chapter 8. A Framework for Microprocessor 
176 
8.1 Introduction 176
8.2 Machine Specification Framework 180
8.3 Microcoded Machine Example 184
8.4 Incremental Model of Control Memory 188
8.5 Summary 192
Chapter 9. Designing a Processor 194
9.1 Instruction Set and Machine Architecture 194
9.2 Top Level Specification 197
9.3 Microcoded Implementation 204
9.4 Low-level Implementation 215
9.5 Conclusions 219
Chapter 10. Hardware Compilation 220
10.1 Introduction 220
10.2 A Language of Communicating Processes 223
10.3 Normal Form Implementation 226
10.4 Reduction to Normal Form 228
10.5 Example Proof 230
10.6 Rapid Prototype Compiler 232
10.7 Mapping Normal Form into Hardware 232
10.8 Conclusions 233
Part V: Technology Transfer 236
Chapter 11. Transfer into Industrial Design 238
11.1 Historical Background 238
11.2 Benefits from Formal Methods 240
11.3 Technology Transfer Problems 241
11.4 Requirements for Transfer of Formal Methods 244
11.5 Methods for Transferring Formal Methods 245
11.6 Technology Transfer from the SAFEMOS Project 247
Appendices: Related Work 250
Appendix A: System Verification and 
252 
A.1 Introduction 252
A.2 Our Philosophy of Systems Verification 254
A.3 Verifying Systems 255
A.4 The CLI Stack and Kit 261
A.5 Extending the Stack 272
A.6 Future Verified Systems 273
A.7 Conclusions 274
Appendix B: The ProCoS Project: 
276 
B.1 Introduction 276
B.2 History and Experience 279
B.3 Requirements Engineering and Duration Calculus 280
B.4 Program Specification and Development 285
B.5 Compiler Correctness 288
B.6 Base Systems 289
B.7 Conclusion 291
Acknowledgements 294
Bibliography 296

Produkt-Details

• Erscheint lt. Verlag: 22.10.2013
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik
• Themenwelt: Technik ► Elektrotechnik / Energietechnik
• ISBN-10: 1-4832-9152-9 / 1483291529
• ISBN-13: 978-1-4832-9152-9 / 9781483291529