Towards Verified Systems
Published in October 1994
Book
Hardback
322 pages
978-0-444-89901-9 (ISBN)
Description
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 foundations, provide one means to help with reducing the risk of inducing 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.
This text 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.
This text 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.
More details
Series
Language
English
Place of publication
Oxford
United Kingdom
Publishing group
Elsevier Science & Technology
Target group
Professional and scholarly
Illustrations
appendices, bibliography
Dimensions
Height: 230 mm
ISBN-13
978-0-444-89901-9 (9780444899019)
Copyright in bibliographic data is held by Nielsen Book Services Limited or its licensors: all rights reserved.
Schweitzer Classification
Other editions
Additional editions
Content
Part 1 Introduction: Safety-Critical Systems and Formal Methods. A brief historical perspective. Safety-critical computer systems. Industrial-scale examples of use. Areas of application of formal methods. Safety standards. Discussion. Overview of the Project. The SAFEMOS project. System modelling. Software development and compilation. Hardware design and compilation. Other SAFEMOS project work. Related work. Conclusion. Part 2 Tools and Models: The HOL Logic and System. Introduction. The HOL logic. The HOL system. Timed Transition Systems. Introduction to TTSs and HOL. Example: A traffic light controller. A real-time temporal logic. Timed transition systems. Timed transition diagrams. Verification. Discussion. Part 3 Software: State Transition Assertions - A Case Study. Introduction. An example - Mult. A more detailed specification of Mult. Determining a machine from a program. State transition assertions. Formal specification of Mult. Correctness of MuItProg. Generating Atomic STAs. Laws for combining STAs. Conclusions. Part 4 A Real-Time Language: The SAFE programming language. Interval model. Interval semantics. SAFE semantics. Laws. Conclusion. Program Compilation. Machine language syntax. Machine Language semantics. Compiler specification. Correctness of compilation. Proof of correctness of compilation. Conclusion. Part 5 Hardware: A Framework for Microprocessor Design. lntroduction. Machine specification framework. Microcoded machine example. Incremental model of control memory. Summary. Designing a Processor. Instruction set and machine architecture. Top-level specification. Microcoded implementation. Low-level implementation. Conclusions. Hardware Compilation. Introduction. A language of communicating processes. Normal form implementation. Reduction to normal form. Example proof. Rapid prototype compiler. Mapping normal form into hardware. Conclusions. Part 6 Technology Transfer: Transfer into Industrial Design. Historical background. Benefits from formal methods. Technology Transfer problems. Requirements for transfer of formal methods. Methods for transferring formal methods. Technology transfer from the SAFEMOS project. Appendices: Related Work. System Verification and the CLI Stack. Introduction. Our philosophy of systems verification. Verifying systems. The CLI stack and kit. Extending the stack. Future verified systems. Conclusions. The ProCoS Project: Provably Correct Systems. Introduction. History and experience. Requirements engineering and duration calculus. Program specification and development. Compiler correctness. Base systems. Conclusion.