4 ms·
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 C
by 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 agoMISRA 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 agoGerard 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 agoAs 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 agoGerard 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 agoI probably should have clicked around a bit to determine that he is the owner of that site :)