Formal Specification and Mechanical Verification of SIFT: A Fault-Tolerant Flight Control System
- 1 July 1982
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-31 (7) , 616-630
- https://doi.org/10.1109/tc.1982.1676059
Abstract
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 refine these 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.Keywords
This publication has 5 references indexed in Scilit:
- SIFT: System Design and ImplementationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Reaching Agreement in the Presence of FaultsJournal of the ACM, 1980
- FTMP—A highly reliable fault-tolerant multiprocess for aircraftProceedings of the IEEE, 1978
- SIFT: Design and analysis of a fault-tolerant computer for aircraft controlProceedings of the IEEE, 1978
- Automatic program verification I: A logical basis and its implementationActa Informatica, 1975