The design verification of a quadruply redundant processor element for high-integrity embedded applications is described. The system, based on the INMOS Transputer, is modeled formally and mathematically proved to be tolerant to any single fault. This was accomplished by formally specifying the correct behavior of the system, as a buffer, and modeling its correct behavior with a composite of the correct behaviors of each of its components. The complete model is demonstrably a refinement of the specification, i.e., better and more ordered.<>


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal verification of a fault tolerant computer


    Contributors:
    Brock, N.A. (author) / Jackson, D.M. (author)


    Publication date :

    1992-01-01


    Size :

    544892 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Verification of a Fault-Tolerant Computer

    Brock, N. / Jackson, D. M. / IEEE et al. | British Library Conference Proceedings | 1992


    Formal Verification for Fault-Tolerant Architectures/PVS Design

    Rushby, J. / United States; National Aeronautics and Space Administration | British Library Conference Proceedings | 1995



    Fault-tolerant computer system

    Avizienis, A. A. / Rennels, D. A. / Ercegovac, M. | NTRS | 1979


    Fault Tolerant Spaceborne Computer

    D. R. Bates / J. E. Schell / G. R. Couranz | NTIS | 1984