Formal verification of algorithms for critical systems
The work
| Authors | John Rushby; Friedrich W. von Henke |
|---|---|
| Editors | |
| Type | article |
| Year | 1993 |
| Citekey | rushby1993formalb |
Where it appeared
| Published in | IEEE Transactions on Software Engineering |
|---|---|
| Publisher | IEEE Computer Society |
| Volume | 19 |
| Issue | 1 |
| Pages | 13--23 |
Identifiers
| DOI | 10.1109/32.210304 |
|---|---|
| OpenAlex | W2114957237 |
Access
| Landing page | https://doi.org/10.1109/32.210304 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
The authors describe their 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. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized.>
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 01:53 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{rushby1993formalb,
title = {Formal verification of algorithms for critical systems},
author = {John Rushby and Friedrich W. von Henke},
year = {1993},
journal = {IEEE Transactions on Software Engineering},
publisher = {IEEE Computer Society},
volume = {19},
number = {1},
pages = {13--23},
doi = {10.1109/32.210304},
}
This record lives at https://refs.drheap.org/rushby1993formalb/ and will keep doing so.