25 May
2023
25 May
'23
9:32 p.m.
On 5/25/23 13:21, Paul Koning via cctalk wrote:
In our particular case, we spend about 10x developing all of the
"safety" collateral (requirement docs, architecture docs, design docs,
etc) than actually writing, debugging and testing the code.
Part of the problem is that most of the automotive safety standards were
developed for fairly simple use cases (1000s to a few 10's of 1000s
lines of code). In our particular case, we're looking at 10's of
millions of lines of code and we've discovered that a lot of the
processes specified by the standards do not scale well to that level of
code. :-/
On May 25, 2023, at 3:30 PM, Chuck Guzis via
cctalk <cctalk(a)classiccmp.org> wrote:
On 5/25/23 10:06, Guy Sotomayor via cctalk wrote:
Yes. The problem is the gap between informal understanding and formal
description. For many programmers, that gap occurs when the program source is created.
If the programs are subjected to formal proofs, the gap occurs when the formal specs are
written.
So such things are largely a non-solution. They may help a little if the gap to the
formal spec is smaller. If, as Guy is saying, the formal spec is larger than the code,
then obviously that won't be the case. The way SPARK works is that you have code and
then can also provide
proofs for the code. Proofs are you might expect are *hard* to write
and in many cases are *huge* relative to the actual code (at least if
you want a platinum level proof).
...and we still get gems like the Boeing
737MAX...
--Chuck Languages other than C and C++ have advantages in that
they detect, or avoid, a whole lot of bugs that C/C++ ignore, like bounds violations or
memory leaks. So Ada can be helpful in that some bugs are harder or impossible to create,
or more likely to be detected in testing. But, in spite of having taken a very
interesting week-long course on program proofs by pioneer E.W. Dijkstra, I don't
actually believe in those things.
I don't either. ;-) Proofs are *hard* and
take a special way of
thinking about the problem. For example, prove that a doubly linked
list points only to elements allowed in the linked list (e.g. things
that have only been placed on the list) and that the forward and
backward pointers actually point to the elements they're supposed
to...and that's one of the simpler things that needs to be proved. It
gets *really* interesting when you try and prove that the scheduler is
actually scheduling the way it's supposed to. :-/
The 737MAX is a classic example of designers turning off their brains before doing their
work. It is obvious even to me (who have never created safety-sensitive software) that
you don't attach systems with single points of failure such as non-replicated sensors
to a control system whose specific purpose is to point the airplane nose DOWN. If you do
your work with your brain disabled you can't produce correct software, with or without
formal proofs.
Yes, in self-driving cars we do "sensor fusion" which
allows us to
derive (and validate/replicate) data from various sensors. For example,
we use cameras, LIDAR, etc to validate each other's data. The point is
to not have a "single point of failure".
--
TTFN - Guy