Engineering topics

Schneider, Fred B.

Publications and source records attributed to Schneider, Fred B..

6 records

NASA NTRS1994

Refinement for fault-tolerance: An aircraft hand-off protocol

Part of the Advanced Automation System (AAS) for air-traffic control is a protocol to permit flight hand-off from one air-traffic controller to another. The protocol must be fault-tolerant and, therefore, is subtle -- an ideal candidate for the application of formal methods. This paper describes a formal method for deriving fault-tolerant protocols that is based on refinement and proof outlines. The AAS hand-off protocol was actually derived using this method; that derivation is given.

Marzullo, Keith↗

NASA NTRS1993

Putting time into proof outlines

A logic for reasoning about timing properties of concurrent programs is presented. The logic is based on Hoare-style proof outlines and can handle maximal parallelism as well as certain resource-constrained execution environments. The correctness proof for a mutual exclusion protocol that uses execution timings in a subtle way illustrates the logic in action. A soundness proof using structural operational semantics is outlined in the appendix.

Schneider, Fred B.↗

NASA NTRS1992

Optimal primary-backup protocols

We give primary-backup protocols for various models of failure. These protocols are optimal with respect to degree of replication, failover time, and response time to client requests.

Budhiraja, Navin↗

NASA NTRS1992

Primary-backup protocols: Lower bounds and optimal implementations

A formal specification of primary-backup is presented. We then prove lower bounds on the degree of replication, failover time, and worst-case response time to client requests assuming different failure models. Finally, we outline primary-backup protocols and indicate which of our lower bounds are tight.

Budhiraja, Navin↗

NASA NTRS1991

Putting time into proof outlines

A logic for reasoning about timing of concurrent programs is presented. The logic is based on proof outlines and can handle maximal parallelism as well as resource-constrained execution environments. The correctness proof for a mutual exclusion protocol that uses execution timings in a subtle way illustrates the logic in action.

Schneider, Fred B.↗

NASA NTRS1991

Derivation of sequential, real-time, process-control programs

The use of weakest-precondition predicate transformers in the derivation of sequential, process-control software is discussed. Only one extension to Dijkstra's calculus for deriving ordinary sequential programs was found to be necessary: function-valued auxiliary variables. These auxiliary variables are needed for reasoning about states of a physical process that exists during program transitions.

Marzullo, Keith↗