Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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