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:[email protected]] Sent: Thursday, August 04, 2016 11:33 AM To: [email protected] 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 <[email protected]> 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 <[email protected]> Mike Cantwell <[email protected]> For policy questions, send mail to: Jim Bacher: <[email protected]> David Heald: <[email protected]>
