ThesaHelp: references pr
ThesaHelp: ACM references mz
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: manmachine 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. 115.
Google
Quotations
3 ;;Quote: an asynchronous, triplyredundant voting system was unstable because channels sampled sensors at different times; bad at control points
 3 ;;Quote: for digital flightcontrol use synchronous channels, sensor data to all channels, and exactmatch majority voting; needs faulttolerant 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
ThesaHelp: references pr (245 items)
ThesaHelp: ACM references mz (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: manmachine symbiosis (46 items)
