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.
Rules for Writing Safety Critical Code (2006)
21–30 of 82 posts
Re: Rules for Writing Safety Critical Code (2006)
#22Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded.
Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems?
I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say, printf. Most of the attempts at formal proof I've seen seem quite complex for very simple functions [1] and the next step up seems too complicated for me to follow [2]. I'm familiar with heuristic-based tools like clang analyser, coverity and flexelint - but none of those claim to produce any sort of proof. I'm also aware of MISRA but again, that doesn't claim to provide any sort of proof.
Those of you who are using formal methods: Is what I've seen really the state of the art? Or are there powerful tools I've overlooked?
[1] https://github.com/Beatgodes/klibc_framac_wp/blob/master/src... [2] https://github.com/seL4/l4v/blob/master/lib/Monad_WP/Strengt...
Re: Rules for Writing Safety Critical Code (2006)
#23What have you guys been using to track requirements? I had a bad experience adapting Redmine for a project, and wouldn't want to repeat that in a next project.
We use DOORS. I don't have experience with other tools, so I can't compare but I don't find it a nice experience either.
Re: Rules for Writing Safety Critical Code (2006)
#24Earlier quoted context omitted.
I would also say perhaps avoid recursion should be revised to avoid non-tail-call recursion Because the justification to avoid recursion is basically avoid running into the limit of stack, and tail-call recursion uses no stack space at all. Of course you still might end up with situations where the function does not terminate, but simple loops can do that too. In relation to Rule No.2, it is also possible to prove an…
Recursion is recursion. Tail recursion is optimized away by the compiler except when it isn't (I've seen bugs with this exact setup more than once), but now you have to verify that the compiler actually does this. It's simpler to just avoid it all together unless you want to formally verify the recursion depth.
Exactly. Tail recursion can always be rewritten as a loop. The code might be uglier but at least you have a better idea of how it's going to behave after compilation.
Re: Rules for Writing Safety Critical Code (2006)
#25What have you guys been using to track requirements? I had a bad experience adapting Redmine for a project, and wouldn't want to repeat that in a next project.
I have heard that Polarion is an ok requirements management tool for software, but it is expensive.
DOORS is good for tracking and tracing requirements, but from what I can see doesn't do code parsing. This may have changed. However, my opinion of IBM software is irreparably broken so I don't have a huge amount of trust in it.
We use Reqtify to glue requirement documents to code. It also sucks, but I think it's still powerful. You just need to set up some regexes which can recognize your requirement identifier style and you're good to go.
Whoever comes up with a solution to glue DOORS requirements to Jira issues to code seamlessly is going to be fairly rich.
Re: Rules for Writing Safety Critical Code (2006)
#26Earlier quoted context omitted.
> An opinionated and needlessly specific list Not really. Gerard Holzmann is in charge of software at NASA/JPL. Each rule comes from experience with a mission loss that would have been prevented if people had implemented that rule. They also help static analysers become more accurate. These rules are specific to ultra-reliable embedded software, flight software or software for life-critical equipment. They are not re…
That doesn't mean that the rules are perfect. There haven't been that many mission losses to have a large corpus of data and finding a root cause of an accident might not lead to the best rules. "The rocket wouldn't have blown up if you asserted this here" doesn't mean that adding a large number assertions necessarily leads to better code.
A lot of wisdom comes from simulations as well.
Re: Rules for Writing Safety Critical Code (2006)
#27I 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.
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]
Re: Rules for Writing Safety Critical Code (2006)
#28Earlier quoted context omitted.
Sure and this list likely worked well in the NASA/JBL context. The point being is it needlessly specific as a generic advice. At the risk of stating the obvious, a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel, which may not be flying every space probe, but it's still pretty damn ultra-reliable piece of software.
Talk about missing the point and the whole context around mission-critical software. > a "goto exit" pattern is the defacto standard for function cleanup in Linux kernel There are many ways to do error cleanup that do not involve goto, and there are many bad ways to use goto. A static analyser can't decide if you do "good goto" or "bad goto", but it's easy to ban goto outright and avoid all the "bad gotos". You pay t…
The Linux kernel is not mission critical? Many of those mission critical systems probably run off of a Linux kernel, you know.
I think the point is that while it is potentially a good rule for mission critical code, it is not essential. There are other ways as well.
Re: Rules for Writing Safety Critical Code (2006)
#29Earlier quoted context omitted.
Recursion is recursion. Tail recursion is optimized away by the compiler except when it isn't (I've seen bugs with this exact setup more than once), but now you have to verify that the compiler actually does this. It's simpler to just avoid it all together unless you want to formally verify the recursion depth.
Apart from that, TCO destroys information that is valuable for debugging (especially for non-recursive tail calls), exactly what you want to avoid in safety-critical software.
Manual conversion to a loop also destroys the same information, so it’s a wash either way on that front.
Re: Rules for Writing Safety Critical Code (2006)
#30Rules like avoiding recursion and loop upper bounds are partly justified by helping code analyzers to prove executions are bounded. Does anyone have experience performing formal static analysis on code? And if so, are there any open-source examples of the state-of-the-art tools being used on nontrivial problems? I've been looking at this recently, but I've never seen a proof of reasonably standard function like, say,…
Take a look at dafny [1] and F* [2]. Both are open-source and it appears that both of them are able to prove code to be correct with considerably less proof code than traditional interactive theorem provers (such as Coq or Isabelle), mostly thanks to the use of an SMT solver (Z3, in both cases) to aid in proving.
Both languages are being used in Project Everest [3], which is building a formally verified HTTPS stack, including a formally verified TLS implementation [4].
Unfortunately, there isn't a lot of documentation / beginner guides about these languages out there, but with the little there is, I was still able to start proving non-trivial (but still relatively easy-to-prove) code with them, even though I have no formal verification background whatsoever.
Just as a tip, I found the Dafny tutorial to be a lot easier to follow than F-Star's, but from what I could gather, F* appears to be slightly more general/sophisticated in what it can prove.
[1] https://github.com/Microsoft/dafny [2] https://www.fstar-lang.org [3] https://project-everest.github.io [4] https://mitls.org