The problem with focusing on the code is that real world experience is that a high percentage of the failures which occur with software related safety are a failure of the original specification for what the software is supposed to do, not failures of the code to do what the programmer intended. Particular problems occur if the limits of operation of the equipment are not properly understood: a classic example being a passenger aircraft crash caused by the avionics being unable to detect when the aircraft wheels had hit the runway in very wet conditions due to aquaplaning whereas in the dry conditions under which the system was tested it worked perfectly.
This is why standards which deal with software in safety related applications (including those derived from IEC 61508, and the medical devices software standard, IEC 62304) focus much more on the overall procedure for specifying and designing the software and then checking that the specification has been met, and are not overly prescriptive about language, structure or other detailed requirements for code. Nick. > On 4 Aug 2016, at 21:49, B Rowland <bfr...@direct.ca> wrote: > > Indeed, Brian, there is a difference between a provably-correct code block, > and actual execution of the code, in other than a dedicated run-time, without > interrupts, or real-time OS, or … interesting point about the core, whether > it has been proven to execute correctly, in every possible case ;-) That's a > couple of test vectors, no? > > Barry > > > > > On 04/08/2016, at 21:23 , Brian O'Connell <oconne...@tamuracorp.com> wrote: > >> Whom considers Ada (the language name is not an acronym) provably correct? >> How do you prove the program is deterministic? What if a Verification >> Condition is not proven? Is the code incorrect? Is the assertion not correct >> or incomplete? Does P = NP ? SPARK 2014 did attempt to address some of this >> stuff, BTW. >> >> Do not think that we will find answers to these questions in ISO8652. What >> Ada does provide is a formalized programming method for concurrency + design >> by contract, which offer a little more hope for code safety and test >> coverage. >> >> The weakness for all human code solutions is a provable processor core where >> the assumption is a provable algorithm. If a static evaluation indicates a >> deterministic algorithm, and if a contract violation occurs at runtime, what >> is 'wrong'? The language? The Compiler? The design assumptions? The >> processor core? Once you get past Ada (or any other language) compile-time >> protection, you return to the electronic jungle where you are part of the >> food chain. >> >> Brian >> >> >> From: B Rowland [mailto:bfr...@direct.ca] >> Sent: Thursday, August 04, 2016 11:33 AM >> To: EMC-PSTC@LISTSERV.IEEE.ORG >> Subject: Re: [PSES] SAFETTY FEATURES controlled by ....SOFTWARE >> >> Hi List-colleagues; >> >> I think, if the safety-related functions are life-critical, they need to be >> written in a "provably-correct" language/environment, like ADA, or some >> equivalent. And, of course, that also means that such functionality needs to >> be isolated from software that is NOT provably-correct (is Windows >> "provably-correct" ?). >> >> In any case, life-critical systems need to be, at least, redundant, with >> fail-safe shutdown if the processes do not agree at timed checkpoints, and >> also have hardware-based watchdog timers (sometimes built-in to the >> microcontroller, itself) to guarantee continued function. Furthermore, it is >> also typical that the software that runs on the redundant processors is >> written by different teams, so that an error in a program on one "side" is >> not duplicated in the other half/third of the redundant CPUs. >> >> Since, as some have pointed out, it is readily-accomplished to have a >> provably-correct hardware implementation of the safety functions that are >> "at the edge" of the system, FPGA's, PALs, etc., with ROM, or >> check-summed-on-load-firmware, are much more reliable.. >> >> In another discussion that I had, a while back, we even discussed how to >> ensure that the semiconductor devices, at the safety interface, are made >> reliable-enough to allow proper operation, even in the typical fail-short >> conditions. I think that this is why we have relays costing > $1000 used in >> train/subway applications ;-) >> >> Cheers, >> Barry Rowland >> Muenchen, Bayern >> >> - >> ---------------------------------------------------------------- >> This message is from the IEEE Product Safety Engineering Society emc-pstc >> discussion list. To post a message to the list, send your e-mail to >> <emc-p...@ieee.org> >> >> All emc-pstc postings are archived and searchable on the web at: >> http://www.ieee-pses.org/emc-pstc.html >> >> Attachments are not permitted but the IEEE PSES Online Communities site at >> http://product-compliance.oc.ieee.org/ can be used for graphics (in >> well-used formats), large files, etc. >> >> Website: http://www.ieee-pses.org/ >> Instructions: http://www.ieee-pses.org/list.html (including how to >> unsubscribe) >> List rules: http://www.ieee-pses.org/listrules.html >> >> For help, send mail to the list administrators: >> Scott Douglas <sdoug...@ieee.org> >> Mike Cantwell <mcantw...@ieee.org> >> >> For policy questions, send mail to: >> Jim Bacher: <j.bac...@ieee.org> >> David Heald: <dhe...@gmail.com> > > - > ---------------------------------------------------------------- > This message is from the IEEE Product Safety Engineering Society emc-pstc > discussion list. To post a message to the list, send your e-mail to > <emc-p...@ieee.org> > > All emc-pstc postings are archived and searchable on the web at: > http://www.ieee-pses.org/emc-pstc.html > > Attachments are not permitted but the IEEE PSES Online Communities site at > http://product-compliance.oc.ieee.org/ can be used for graphics (in well-used > formats), large files, etc. > > Website: http://www.ieee-pses.org/ > Instructions: http://www.ieee-pses.org/list.html (including how to > unsubscribe) > List rules: http://www.ieee-pses.org/listrules.html > > For help, send mail to the list administrators: > Scott Douglas <sdoug...@ieee.org> > Mike Cantwell <mcantw...@ieee.org> > > For policy questions, send mail to: > Jim Bacher: <j.bac...@ieee.org> > David Heald: <dhe...@gmail.com> - ---------------------------------------------------------------- This message is from the IEEE Product Safety Engineering Society emc-pstc discussion list. To post a message to the list, send your e-mail to <emc-p...@ieee.org> All emc-pstc postings are archived and searchable on the web at: http://www.ieee-pses.org/emc-pstc.html Attachments are not permitted but the IEEE PSES Online Communities site at http://product-compliance.oc.ieee.org/ can be used for graphics (in well-used formats), large files, etc. Website: http://www.ieee-pses.org/ Instructions: http://www.ieee-pses.org/list.html (including how to unsubscribe) List rules: http://www.ieee-pses.org/listrules.html For help, send mail to the list administrators: Scott Douglas <sdoug...@ieee.org> Mike Cantwell <mcantw...@ieee.org> For policy questions, send mail to: Jim Bacher: <j.bac...@ieee.org> David Heald: <dhe...@gmail.com>
