Originally Posted by
bsieker
That is possibly the worst suggestion so far.
Assembly code is almost impossible to analyse for correctness in any meaningful way. It is far better (and provably so) to write in a well-specified (i. e. not C) language, prove the source code correct (for which scalable and practical techniques exist today), or define and prove correct a finite state machine and have code generated from it.
I would assume that it is either SCADE, or Simulink.
Both tools generate C code, but with SCADE you don't have to inspect the C once the tool chain have been qualified. (Considered the safest alternative of the two)
SCADE is used by Airbus (Both French products), and Boeing might use Simulink.
But this is irrelevant for this discussion since the fault is in the specification, not the software.