3 ms·

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 wan

by ti32x 10y ago

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.

nstj 10y ago
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 http://spinroot.com/gerard/pdf/P10.pdf
- pjmlp 10y ago
  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/ http://frama-c.com/ https://www.securecoding.cert.org/confluence/display/seccode/SEI+CERT+Coding+Standards 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).
- mos_basik 10y ago
  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.
  - 4ad 10y ago
    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.
  - mturmon 10y ago
    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.
  - nstj 10y ago
    I probably should have clicked around a bit to determine that he is the owner of that site :)
kejaed 10y ago
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.
danjayh 10y ago
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.

by ti32x 10y ago

nstj 10y ago

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 http://spinroot.com/gerard/pdf/P10.pdf

pjmlp 10y ago
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/ http://frama-c.com/ https://www.securecoding.cert.org/confluence/display/seccode/SEI+CERT+Coding+Standards 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).
mos_basik 10y ago
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.
- 4ad 10y ago
  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.
- mturmon 10y ago
  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.
- nstj 10y ago
  I probably should have clicked around a bit to determine that he is the owner of that site :)

kejaed 10y ago

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.

danjayh 10y ago

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.