Abstract
We present the formal verification of synchronizing aspects of the Reliable Computing Platform (RCP), a fault-tolerant computing system for digital flight control applications. The RCP uses NMR-style redundancy to mask faults and internal majority voting to purge the effects of transient faults. The system design has been formally specified and verified using the Ehdm verification system. Our formalization is based on an extended state machine model incorporating snapshots of local processors’ clocks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
W. R. Bevier, W. D. Young. The proof of correctness of a fault-tolerant circuit design. Second IFIP Conference on Dependable Computing For Critical Applications, Tucson, Arizona, February 1991, pp. 107-114.
R. W. Butler, J. L. Caldwell, B. L. Di Vito. Design strategy for a formally verified reliable computing platform. 6th Annual Conference on Computer Assurance (COMPASS 91), Gaithersburg, MD, June 1991.
R. W. Butler, B. L. Di Vito. Formal design and verification of a reliable computing platform for real-time control (phase 2 results). NASA Technical Memorandum 104196, January 1992.
B. L. Di Vito, R. W. Butler, J. L. Caldwell. High level design proof of a reliable computing platform. Dependable Computing for Critical Applications 2, Dependable Computing and Fault-Tolerant Systems, Springer Verlag, Wien New York, 1992, pp. 279–306. Also presented at 2nd IFIP Working Conference on Dependable Computing for Critical Applications, Tucson, AZ, Feb. 18–20, 1991, pp. 124-136.
B. L. Di Vito, R. W. Butler, J. L. Caldwell, II. Formal design and verification of a reliable computing platform for real-time control (phase 1 results). NASA Technical Memorandum 102716, October 1990.
J. Goldberg et al. Development and analysis of the software implemented fault-tolerance (SIFT) computer. NASA Contractor Report 172146, 1984.
A. L. Hopkins, Jr., T. Basil Smith, III, J. H. Lala. FTMP — A highly reliable fault-tolerant multiprocessor for aircraft. Proc. IEEE, 66(10), October 1978, pp. 1221–1239.
H. Kopetz, A. Damm, C. Koza, M. Mulazzani, W. Schwabl, C. Senft, R. Zainlinger. Distributed fault-tolerant real-time systems: The Mars approach. IEEE Micro, 9, February 1989, pp. 25–40.
J. H. Lala, L. S. Alger, R. J. Gauthier, M. J. Dzwonczyk. A Fault-Tolerant Processor to meet rigorous failure requirements. Technical Report CSDL-P-2705, Charles Stark Draper Lab., Inc., July 1986.
L. Lamport, P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1), January 1985, pp. 52–78.
L. Lamport, R. Shostak, M. Pease. The Byzantine Generals problem. ACM Transactions on Programming Languages and Systems, 4(3), July 1982, pp. 382–401.
L. V. Mancini, G. Pappalardo. Towards a theory of replicated processing. Lecture Notes in Computer Science, Vol. 331, Springer Verlag, 1988, pp. 175–192.
L. Moser, M. Melliar-Smith, R. Schwartz. Design verification of SIFT. NASA Contractor Report 4097, September 1987.
NASA. Peer review of a formal verification/design proof methodology. NASA Conference Publication 2377, July 1983.
J. Rushby. Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems. NASA Contractor Report 4384, July 1991.
J. Rushby. Formal specification and verification of a fault-masking and transient-recovery model for digital flight-control systems. Second International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Nijmegen, The Netherlands, January 1992, pp. 237-258, Vol. 571, Lecture Notes in Computer Science, Springer Verlag.
J. Rushby, F. von Henke. Formal verification of a fault-tolerant clock synchronization algorithm. NASA Contractor Report 4239, June 1989.
T. Schubert, K. Levitt. Verification of memory management units. Second IFIP Conference on Dependable Computing For Critical Applications, Tucson, Arizona, February 1991, pp. 115-123.
N. Shankar. Mechanical verification of a schematic Byzantine clock synchronization algorithm. NASA Contractor Report 4386, July 1991.
N. Shankar. Mechanical verification of a generalized protocol for byzantine fault-tolerant clock synchronization. Second International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Nijmegen, The Netherlands, January 1992, pp. 217–236, Vol. 571 of Lecture Notes in Computer Science, Springer Verlag.
M. Srivas, M. Bickford. Verification of the FtCayuga fault-tolerant microprocessor system (Volume 1: A case study in theorem prover-based verification). NASA Contractor Report 4381, July 1991.
F. W. von Henke, J. S. Crow, R. Lee, J. M. Rushby, R. A. Whitehurst. Ehdm verification environment: an overview. 11th National Computer Security Conference, Baltimore, Maryland, 1988.
C. J. Walter, R. M. Kieckhafer, A. M. Finn. MAFT: a multicomputer architecture for fault-tolerance in real-time control systems. IEEE Real-Time Systems Symposium, December 1985.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag Wien
About this paper
Cite this paper
Di Vito, B.L., Butler, R.W. (1993). Formal Techniques for Synchronized Fault-Tolerant Systems. In: Landwehr, C.E., Randell, B., Simoncini, L. (eds) Dependable Computing for Critical Applications 3. Dependable Computing and Fault-Tolerant Systems, vol 8. Springer, Vienna. https://doi.org/10.1007/978-3-7091-4009-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-7091-4009-3_7
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-4011-6
Online ISBN: 978-3-7091-4009-3
eBook Packages: Springer Book Archive