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

Hi!

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-medical-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)