[SystemSafety] More .....

[Peter Bernard Ladkin]

On 2020-07-10 14:53 , David Crocker wrote:
> 
> 
> The statistical correctness of the code sounds to me beyond the realm of automatic verification;

Coals to Newcastle, maybe, but CbyC, and use of FM, does not depend on *automatic* verification.

If you have code whose output is asserted/desired to have certain statistical properties, such as a
pseudo-random number generator, then in principle you can run Monte Carlo simulations sufficient to
determine to a given confidence (not 100%) that the output has those properties.

That is just as much a FM as anything else, and it is just as much a proof as anything else.

Calling Monte Carlo simulations "unit tests" seems to me to be inappropriate. And if you are not
doing Monte Carlo simulations then you are not justified in confidently drawing a conclusion that
the SW is fit for purpose. (Of couse, you might not care to be very confident.)

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
Styelfy Bleibgsnd
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20200710/119dc693/attachment.sig>