UK Defense software standard

Sean Matthews  
Fri, 30 Jun 89 13:49:12 BST


I have just seen a copy of the UK department of defence draft standard
for safety critical software  (00-55).

Here are a few high (and low) points.

1. There should be no dynamic memory allocation (This rules out explicit
recursion - though a bounded stack is allowed).

2. There should be no interupts except for a regular clock interupt.

3. There should not be any distributed processing (i.e. only a single
processor).

4. There should not be any multiprocessing.

5. NO ASSEMBLER.

6. All code should be at least rigourously checked using mathematical
methods.

7. Any formally verified code should have the proof submitted as well, in
machine readable form, so that an independent check can be performed.

8. All code will be formally specified.

9. There are very strict requirements for static analysis (no unreachable
code, no unused variables, no unintialised variables etc.).

10. No optimising compilers will be used.

11. A language with a formally defined syntax and a well defined semantics,
or a suitable subset thereof will be used.

Comments.

1. means that all storage can be statically allocated.  In fact somewhere it
says that this should be the case.

2-4 seem to leave no option but polling.  This is impractical, especially in
embedded systems.  No one is going to build a fly by wire system with those
sorts of restrictions. (maybe people should therefore not build fly by wire
systems, but that is another matter that has been discussed at length here
already).  it also ignores the fact that there are proof methods for dealing
with distributed systems.

5. This is interesting, I seem to remember reading somewhere that Nasa used
to have the opposite rule: no high level languages, since they actually read
the delivered binary to check that the software did what it was supposed to
do.

6-7.  All through the draft the phrase `mathematical methods' or `formal
methods' is *invoked* in a general way without going into very much detail
about what is involved.  I am not sure that the people who wrote the report
were sure (Could someone from Praxis - which I believe consulted on drawing
it up - enlarge on this?).

8. this is an excellent thing, though it does not say what sort of language
should be used.  Is a description in terms of a Turing machine suitable?
After all that is a well understood formal system.

10. Interestingly, there is no requirement that the compiler be formally
verified, just that it should conform to international standards (though
strictly), and not have any gross hacks (i.e. optimisation) installed.
There is also no demand that the target processor hardware be verified
(though such a device exists here already: the Royal Signals Research
Establishment's Viper processor).

11. seems to be a dig at Ada and the no subsets rule.  It also rules out C.

Conclusions.

I find the idea of the wholesale mayhem and killing merchants being forced
to try so much harder to ensure that their products maim and kill only the
people they are supposed to maim and kill, rather amusing.

The standard seems to be naive in its expectations of what can be achieved
at the moment with formal methods (That is apparently the general opinion
around here, and there is a *lot* of active research in program verification
in Edinburgh), and impossibly restrictive.

An interesting move in the right direction but too fast and too soon.  And
they might blow the idea of Formal verification by tring to force it too
soon.  And I would very much like to see these ideas trickle down into the
civil sector.

I might follow this up with a larger (and more coherent) description if
there is interest (this was typed from memory after seeing it yesterday)
there is quite a bit more in it.

Sean Matthews
Dept. of Artificial Intelligence JANET: sean@uk.ac.ed.aipna
University of Edinburgh           ARPA: sean%uk.ac.ed.aipna@nsfnet-relay.ac.uk
80 South Bridge                   UUCP: ...!mcvax!ukc!aipna!sean
Edinburgh, EH1 1HN, Scotland