--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - sufficiency of proofs



Hello,

thanks a lot for your clarification,
it was eye-opening for me.

Regards,
Kerstin



> This is an interesting question, and I am not surprised
> that you found different answers for it. I will provide one
> point of view.

> > I wonder about a general question. When is a proof considered to be
> > sufficient and exhaustive?

> It all depends on the objectives you have. It is not
> our (us tool providers) place to define them.

> To use an example, avionics software is usually written
> according to the guidelines defined in the DO-178B. The
> DO-178B is a rather general document, and the way it
> is actually implemented (by the aircraft manufacturer)
> is checked by the appropriate authority (the FAA, the EASA).
> In the DO-178B, tools that are used in the process have
> to be qualified (by the manufacturer): as development tools
> for things such as compilers, and as verification tools
> for tools used in verification. The qualification of a tool
> as development tool is an extremely heavy process.
> In comparison, the qualification as a verification tool is
> lighter, but still a significant piece of work.

> The aircraft manufacturer, not the tool provider, defines
> the usage that is made of the tool during the verification
> process, and shows the steps that were taken in order to
> check that the tool could be used reliably for this purpose.
> According to http://en.wikipedia.org/wiki/DO-178B ,
> *comprehensive* (emphasis mine) black-box testing is
> currently judged sufficient for qualifying a tool as a
> verification tool.

> In short, if you need to trust any part of the Frama-C platform,
> you should first define your needs and make sure yourself that
> it suits them.

> Best regards,

> Pascal

> PS: I will be immodest enough to point to
>
http://rdn-consulting.com/blog/2009/06/04/guest-article-static-analysis-in-m
edical-device-software-part-2-methodology/
> and I also recommend the last section of http://tr.im/RPFeynman
> for an overview of how software verification works
> (although the Shuttle's software was verified using
> testing techniques only, to the best of my knowledge)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/ms-tnef
Size: 3897 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090723/287ba22a/attachment.bin