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 <[email protected]> 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:[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]> - ---------------------------------------------------------------- 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]>
