[SystemSafety] Fwd: Re: CbyC and unit testing
Olwen Morgan
olwen at phaedsys.com
Mon Jul 6 20:01:53 CEST 2020
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
More information about the systemsafety
mailing list