Nose Gear Example

To stimulate and unify the discussions, we developed a common example that was addressed by the speakers and participants. Here is a sample pseudo code that implements the functions described in the example. Please note that the pseudo code has not been compiled or checked in any way by a software tool. The code has been seeded intentionally with a few defects and other aberrations (just to make it interesting!). The required behavior is specified on the first page of the pseudo code along with assumptions.

We encouraged the participants to approach this example from various angles and varying levels (e.g., actual code vs. formal model vs. assurance case).

This example involves a variety of different kinds of complexities which are an opportunity to demonstrate the flexibility of a theorem proving approach, e.g., reasoning about timing relationships, arithmetic calculations, and non-trivial decision logic.

A preliminary list of questions and comments which were addressed by the participants in the context of this example is given below.

Maintained by Mike Gordon.
This page last updated on Mon Nov 11 2013.