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


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Formal verification of a fault tolerant computer


    Beteiligte:
    Brock, N.A. (Autor:in) / Jackson, D.M. (Autor:in)


    Erscheinungsdatum :

    01.01.1992


    Format / Umfang :

    544892 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    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 Spaceborne Computer

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


    Fault-tolerant computer system

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