[SystemSafety] Fwd: Re: CbyC and unit testing

[Olwen Morgan]

On 06/07/2020 18:14, Martyn Thomas wrote:
> On 05/07/2020 11:00, Olwen Morgan wrote:
>
>> Counter question:
>>
>> If you are using CbyC and a system unit fails under test at a stage of
>> testing later than UT, what do you do?
>>
> In principle,  work back to where the error was introduced, correct the
> error there and develop forward from there. Later, look at the
> intermediate steps to see the earliest point where the error should have
> been detected and improve the process or the tools.
>
Progress! :-)))

Some of the questions are receiving helpful answers, for which Martyn is 
due and has my thanks. ... PBL-of-the-empty-chair-persuasion, take note 
... ;-)

I agree with this answer as far as it goes - although the "in principle" 
bit begs further substantial questions. But what if you find that the 
problem has arisen from any of:

1. Failure to meet a requirement that the formal proofs specifying the 
black-box behaviour of software units do not and cannot capture? E.g. a 
non-functional requirement. I could easily give you a terrifying example 
from the software that controls a medical ventilator designed for use 
with premature neonates experience acute respiratory distress.

2. Problems in the proof tools including any of:

     2.a Failure correctly to capture the semantics of the language as 
implemented by the compiler? E.g. by incorrect handling of 
implementation-defined and implementation-dependent features. This is a 
nightmare in C and, though I'd expect it to be less of a problem in 
SPARK Ada, the mere fact of difficulties in other languages makes the 
question legitimate.

     2.b Failure of the compiler correctly to meet the requirements of 
the language standard or the compiler's having used in perverse ways the 
latitude that the standard leaves to the implementor? Again a potential 
nightmare in C, so what about SPARK Ada?

     2.c Failure of the configuration control process to keep technical 
control of the produced system artefacts and the tools themselves? I 
could give you some risible examples from the development of telecom 
network management software.

3. Failure of the formal specification to capture all of the functional 
requirements that were contained in the initial (presumed) natural 
language system functional requirements specification?

Your answer covers these cases, but each of them gives reason to 
question the *unqualified* claim that proof of correctness assures that 
no errors will be found in UT and that, therefore, UT may be avoided- or 
at least *safely* avoided, if only because, with the possible exception 
of case 3, in these cases UT would provide the earliest possible 
opportunity to determine that the produced artefact was not meeting the 
requirements.


Olwen