News for hackers. Stuff that matters.
Re:Rules for Writing Safety Critical Code (2006) by ti32x on Friday November 04, 2016 @06:48AM (#12871596)
I work on software that goes to space. I believe we and NASA use the MISRA coding standard, which is effectively this but taken to extremes. If you actually want to create safety critical code I would recommend that you familiarize yourself with the MISRA ruleset and DO-178B.
Re:Rules for Writing Safety Critical Code (2006) by kejaed on Friday November 04, 2016 @10:35AM (#12872842)
If anyone is looking into this sort of stuff, you can check out the relatively new DO-178C as well, which adds some more details about tool qualification, formal methods, and model-based development. Signed, your friendly neighbourhood aerospace systems engineer.
Re:Rules for Writing Safety Critical Code (2006) by nstj on Friday November 04, 2016 @07:50AM (#12871836)
Space software? Nice! Going to check out MISRA now.

FWIW the initial page just reflects the JPL publication "The Power of Ten – Rules for Developing Safety Critical Code" by Gerard Holzmann [0]

[0]: http://spinroot.com/gerard/pdf/P10.pdf

Re:Rules for Writing Safety Critical Code (2006) by pjmlp on Friday November 04, 2016 @08:40AM (#12872057)
MISRA only goes thus far.

For writing safe code in C, you should also check Frama-C and CERT Secure Coding Standards.

http://frama-c.com/

https://www.securecoding.cert.org/confluence/display/seccode...

Even better, get the algorithms written in a theorem prover which is guaranteed to generate reliable safe C code.

This is approach taken by Microsoft with P Language(Windows USB device driver stack) and F* (new TLS implementation).

Re:Rules for Writing Safety Critical Code (2006) by mos_basik on Friday November 04, 2016 @11:38AM (#12873404)
Gerard Holzmann is the main author of the formal software verification tool "spin" as well as the owner of spinroot.com. I took a class on formal verification under him at Caltech.
Re:Rules for Writing Safety Critical Code (2006) by 4ad on Friday November 04, 2016 @11:44AM (#12873459)
As an anecdote, spin was used in Plan 9 to validate the kernel scheduler and the IL network protocol. It was also used to validate a very early version of the Go scheduler.
Re:Rules for Writing Safety Critical Code (2006) by mturmon on Friday November 04, 2016 @12:01PM (#12873585)
Gerard is an ACM Fellow and a member of the NAE, and has been a leader in reliable software for NASA since he came to JPL from Bell Labs.
Re:Rules for Writing Safety Critical Code (2006) by nstj on Friday November 04, 2016 @02:59PM (#12874998)
I probably should have clicked around a bit to determine that he is the owner of that site :)
Re:Rules for Writing Safety Critical Code (2006) by danjayh on Saturday November 05, 2016 @01:07AM (#12878287)
I work for your friendly Aviation megacorp producing avionics-related widgets. We are currently transitioning to DO-178C. Fun anecdote: I took a training class on Peach Fuzzer last year & got to hear people from MS, Mozilla, etc. talk about the testing they do on their software. I asked them if they ever had to prove things like worst-case execution time, worst-case stack utilization, perform MC/DC analysis, perform source-to-object analysis, etc., etc. They did not ... and that, my friends, is why avionics software is so damned expensive compared to other software :)

EDIT: And to those of you debating whether all of these rules are necessary and good -- they are; however, they are a subset. We use an internal coding standard that resembles MISRA C but does have some modifications. The only rule of his that we don't do nearly the same way is the 60 line limit. We use code complexity metrics rather than a strict line limit, but it's the same idea.