NTRS - NASA Technical Reports Server

As of October 27, 2023, NASA STI Services will no longer have an embargo for accepted manuscripts. For more information visit NTRS News.

Back to Results
Formal verification of algorithms for critical systemsWe describe our experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. First, we explain the problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization. We give an overview of one such algorithm, and of the arguments for its correctness. Next, we describe a verification of the algorithm that we performed using our EHDM system for formal specification and verification. We indicate the errors we found in the published analysis of the algorithm, and other benefits that we derived from the verification. Based on our experience, we derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. Finally, we summarize our conclusions regarding the benefits of formal verification in this domain, and the capabilities required of verification systems in order to realize those benefits.
Document ID
Document Type
Reprint (Version printed in journal)
External Source(s)
Rushby, John M.
(SRI International, Computer Science Lab. Menlo Park, CA, United States)
Von Henke, Friedrich
(Ulm Univ. Germany)
Date Acquired
August 16, 2013
Publication Date
January 1, 1993
Publication Information
Publication: IEEE Transactions on Software Engineering
Volume: 19
Issue: 1
ISSN: 0098-5589
Subject Category
Computer Programming And Software
Accession Number
Funding Number(s)
Distribution Limits

Available Downloads

There are no available downloads for this record.
No Preview Available