Abstract
During the last five years industry has progressively spread the use of commercial microprocessors into many areas of real-time control. This has been particularly marked in military projects and has happened in a number of civil applications, such as control of nuclear reactors and railway signalling. Some of these applications are ‘safety-critical’ in the sense that design errors could result in accidents and loss of life. Good examples of such critical applications are found in the avionics fitted in civil and military aircraft [5].
This paper is Copyright ©HMSO London 1986.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bramson B. D., “Malvern’s Program Analysers”, RSRE Research Review 1985.
Carre B. A. and Debney C., “SPADE Pascal”, Program Validation Ltd., UK, July 1985.
Cohn A. and Gordon M. J. C., “A Mechanized Proof of Correctness of a Simple Counter”, University of Cambridge Computer Laboratory, Technical Report No. 94, July 1986.
Cohn A., “A Proof of Correctness of the VIPER Microprocessor: The First Level”, in: VLSI Specification, Verification and Synthesis, (this volume).
Cullyer W. J., “Hardware Integrity”, Aeronautical Journal, Royal Aeronautical Society, UK, September 1985.
Cullyer W. J., “VIPER Microprocessor: Formal Specification”, RSRE Report 85013, October 1985.
Cullyer W. J., “VIPER: Correspondence Between Specification and Major State Machine”, RSRE Report 86004, January 1986.
Cullyer W. J. and Kershaw J., “Programming the VIPER Microprocessor” Proceedings of Conference on Safety and Security, Glasgow, UK, October 1986.
Gordon M. J. C., “LCF-LSM”, University of Cambridge Computer Laboratory, Technical Report No. 41, 1983.
Morison J. et al., “ELLA: Hardware Description or Specification?”, Proceedings IEEE International Conference, CAD-84, Santa Clara, November 1984.
Pygott C. H., “Formal Proof of Correspondence Between a Hardware Module and its Gate Level Implementation”, RSRE Report 85012, June 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1988 Kluwer Academic Publishers, Boston
About this chapter
Cite this chapter
Cullyer, W.J. (1988). Implementing Safety-Critical Systems: The VIPER Microprocessor. In: Birtwistle, G., Subrahmanyam, P.A. (eds) VLSI Specification, Verification and Synthesis. The Kluwer International Series in Engineering and Computer Science, vol 35. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-2007-4_1
Download citation
DOI: https://doi.org/10.1007/978-1-4613-2007-4_1
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-9197-8
Online ISBN: 978-1-4613-2007-4
eBook Packages: Springer Book Archive