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 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 investigate