--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on July 2009 ---
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