### 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.

- The requirements specification is not precise, e.g., what does
“accurate” mean? What about when the aircraft is being pushed
backwards – is this a negative velocity?
- The finite size of the data values (i.e., 16 bits) introduces
some complications that would make the conventional verification by
means of testing more challenging.
- The asynchronous relationship between invocations of the update
function and updates to the two counters introduces some complications
that would also make conventional verification very challenging.
- There are about a dozen assumptions that need to be made, e.g.,
the maximum acceleration of the aircraft on the ground, the amount of
variability in the timing of the pulse generated by the
electro-mechanical sensor connected to the nose gear wheel. Discovering
and formalizing these assumptions may be one of the most interesting
aspects of the assurance cases.

Maintained by Mike Gordon.

This page last updated on Mon Nov 11 2013.