Map
Index
Random
Help
th

QuoteRef: rushJ12_1991

topics > all references > ThesaHelp: references p-r



ThesaHelp:
references p-r
ThesaHelp:
ACM references m-z
Topic:
resourceful, redundant systems for reliability
Topic:
asynchronous processing
Topic:
hard real time systems
Topic:
safety critical systems
Topic:
hardware for interprocess communication
Topic:
synchronized processing
Group:
program proving
Topic:
theorem proving systems
Topic:
man-machine symbiosis

Reference

Rushby, J., von Henke, F., "Formal verification of algorithms for critical systems", Proceedings of the ACM SIGSOFT '91 Conference on Software for Critical Systems, Software Engineering Notes, 16, 5, December 1991, pp. 1-15. Google

Quotations
3 ;;Quote: an asynchronous, triply-redundant voting system was unstable because channels sampled sensors at different times; bad at control points
3 ;;Quote: for digital flight-control use synchronous channels, sensor data to all channels, and exact-match majority voting; needs fault-tolerant clock synchronization, etc.
6 ;;Quote: formally verified Byzantine failure clock synchronization with EHDM; difficult; found many errors, though none serious
7 ;;Quote: using an interactive proof system produced a publishable proof, enumeration of all assumptions, and exploration of changed assumptions
11 ;;Quote: an automatic theorem prover may be worse; no human review and no help with discovering proof errors; should automate calculations, etc.
12 ;;Quote: need interactive system for effective theorem proving; users provide strategy and insights, computers do the calculations
12 ;;Quote: an interactive proof should produce a publishable proof and a robust, strategy for automating the proof
13 ;;Quote: a theorem prover acts as an implacable skeptic that insists on stated assumptions and justified claims; not an oracle


Related Topics up

ThesaHelp: references p-r (245 items)
ThesaHelp: ACM references m-z (280 items)
Topic: resourceful, redundant systems for reliability (35 items)
Topic: asynchronous processing (30 items)
Topic: hard real time systems (64 items)
Topic: safety critical systems (32 items)
Topic: hardware for interprocess communication (31 items)
Topic: synchronized processing (35 items)
Group: program proving   (10 topics, 310 quotes)
Topic: theorem proving systems (20 items)
Topic: man-machine symbiosis (46 items)

Collected barberCB 3/93
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.