This paper describes the formal specification and proof methodology employed to demonstrate that the SIFT computer meets its requirements. The hierarchy of design specifications is shown, from very abstract descriptions of system function down to the implementation. The most abstract design specifications are simple and easy to understand, almost all details of the realization having been abstracted out, and can be used to ensure that the system functions reliably and as intended. A succession of lower level specifications into more detailed and more complex views of the system design, culminating in the Pascal implementation. The paper describes the rigorous mechanical proof that the abstract specifications are satisfied by the actual implementation.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal specification and mechanical verification of SIFT: A fault-tolerant flight control system


    Additional title:

    Formale Spezifikation und mechanische Verifikation von SIFT: ein fehlertolerantes Flugkontrollsystem


    Contributors:

    Published in:

    Publication date :

    1982


    Size :

    15 Seiten, 9 Bilder, 11 Quellen



    Type of media :

    Article (Journal)


    Type of material :

    Print


    Language :

    English




    Hierarchical specification of the SIFT fault tolerant flight control system

    Melliar-Smith, P.M. / Schwartz, R.L. | Tema Archive | 1981


    Formal Verification of a Fault-Tolerant Computer

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


    Fault-tolerant software - Experiment with the sift operating system

    BRUNELLE, J. / ECKHARDT, JR., D. | AIAA | 1985


    Fault-tolerant software - Experiment with the sift operating system

    Brunelle, J. E. / Eckhardt, D. E., Jr. | NTRS | 1985


    SIFT: Design and analysis of a fault-tolerant computer for aircraft control

    Wensley, J.H. / Lamport, L. / Goldberg, J. | Tema Archive | 1978