Advertisement

Formal Techniques for Synchronized Fault-Tolerant Systems

  • Ben L. Di Vito
  • Ricky W. Butler
Part of the Dependable Computing and Fault-Tolerant Systems book series (DEPENDABLECOMP, volume 8)

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.

Keywords

Clock Time Formal Technique Clock Synchronization Transient Fault Dependable Computing 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    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.Google Scholar
  2. [2]
    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.Google Scholar
  3. [3]
    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.Google Scholar
  4. [4]
    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.Google Scholar
  5. [5]
    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.Google Scholar
  6. [6]
    J. Goldberg et al. Development and analysis of the software implemented fault-tolerance (SIFT) computer. NASA Contractor Report 172146, 1984.Google Scholar
  7. [7]
    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.CrossRefGoogle Scholar
  8. [8]
    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.CrossRefGoogle Scholar
  9. [9]
    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.Google Scholar
  10. [10]
    L. Lamport, P. M. Melliar-Smith. Synchronizing clocks in the presence of faults. Journal of the ACM, 32(1), January 1985, pp. 52–78.MathSciNetMATHCrossRefGoogle Scholar
  11. [11]
    L. Lamport, R. Shostak, M. Pease. The Byzantine Generals problem. ACM Transactions on Programming Languages and Systems, 4(3), July 1982, pp. 382–401.MATHCrossRefGoogle Scholar
  12. [12]
    L. V. Mancini, G. Pappalardo. Towards a theory of replicated processing. Lecture Notes in Computer Science, Vol. 331, Springer Verlag, 1988, pp. 175–192.CrossRefGoogle Scholar
  13. [13]
    L. Moser, M. Melliar-Smith, R. Schwartz. Design verification of SIFT. NASA Contractor Report 4097, September 1987.Google Scholar
  14. [14]
    NASA. Peer review of a formal verification/design proof methodology. NASA Conference Publication 2377, July 1983.Google Scholar
  15. [15]
    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.Google Scholar
  16. [16]
    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.Google Scholar
  17. [17]
    J. Rushby, F. von Henke. Formal verification of a fault-tolerant clock synchronization algorithm. NASA Contractor Report 4239, June 1989.Google Scholar
  18. [18]
    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.Google Scholar
  19. [19]
    N. Shankar. Mechanical verification of a schematic Byzantine clock synchronization algorithm. NASA Contractor Report 4386, July 1991.Google Scholar
  20. [20]
    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.CrossRefGoogle Scholar
  21. [21]
    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.Google Scholar
  22. [22]
    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.Google Scholar
  23. [23]
    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.Google Scholar

Copyright information

© Springer-Verlag Wien 1993

Authors and Affiliations

  • Ben L. Di Vito
    • 1
  • Ricky W. Butler
    • 2
  1. 1.VíGYAN, Inc.HamptonUSA
  2. 2.NASA Langley Research CenterHamptonUSA

Personalised recommendations