Rules for Writing Safety Critical Code (2006)

Ask HN mods: How is this URL different from the one in https://news.ycombinator.com/item?id=12864032? I was under impression that submissions are unique...

This doesn't always work, for whatever reason. I've had this as well, but there's not much you can do. The Upvote game isn't that important, so don't lose sleep about it. Check the FAQ first, but send an email to HN support if it's a bug.

SpaceX uses VxWorks for their hard real-time requirements: http://blogs.windriver.com/vxworks/2010/12/vxworks-helping-c...

They use Linux for non-hard-real-time stuff. Their microcontrollers also do not use Linux.

Coincidentally, Tesla uses QNX.

Overall, one way to look at formal methods is that the tools range from fully automated (e.g., abstract interpretation, model checking), to manual (e.g., interactive theorem proving). Along this same range, the complexity of properties which can be proved also moves from simple (e.g., absence of buffer overflows) to complex (termination of parameterized systems).

As a concrete example, interactive theorem provers can prove the termination of Paxos for an arbitrary number of nodes (i.e., a system of `n` nodes will reach consensus, where `n` is a positive integer). But, automatically generating such a proof for something as complicated and parameterized as Paxos is an open problem ([1] describes an automatic tool working toward that goal).

Another thing to keep in mind is the goal of the tool: verification versus bug hunting. Verification aims to prove that a property will never be violated, while bug hunting aims to find a property violation. Here's a list of some types of tools off the top of my head.

Bounded model checkers such as CBMC [2] essentially search the entire state-space of the program; you can conceptually think of this as searching through a graph which has some start node, and you'd like to find a path from the start to an error. This is a bug hunting technique since the software/hardware may have an infinite state space (e.g., `while (true) ++i`), hence the search space must be bounded (e.g., unroll loops). For finite-state systems this can generate proofs of correctness. For infinite state systems, it can generate proofs up to a certain bound (e.g., correct for some number of clock cycles, correct for some number of loop iterations). The benefit of bounded model checkers is that when they find an error they generate a counter-example, which is essentially inputs to the program causing it to fail. So, you could use the counter-example as a concrete test case to fix the issue. Techniques such as counter-example guided abstraction refinement, and more recently IC3 and property-directed reachability make use of these counter-examples to generate proofs for infinite state systems.

A complementary technique is abstract interpretation, and numerical abstract interpretation in particular. One successful tool is Astree, though closed source, has been used to verify properties on Airbus planes. Abstract interpretation is complementary to something like bounded-model checking since it can be used to verify properties on infinite state systems. Numerical abstract interpretation can be used to generate numerical proofs such as, "on line 10, variable `x` is in the range `[-10, 10]`, or constraints between variables such as `x - y >= 10`. A difficult part with abstract interpretation, however, is that when it reports an error it may be the case that the error is a false-alarm and it doesn't actually exist. You can think of numerical abstract interpretation as typical "compiler algorithms" such as constant propagation but keeping track of much more complicated information.

Symbolic/Concolic execution, such as KLEE [4], Pex and Moles [5], and their successor IntelliTest [6], are sort of a middle ground between model checking, and traditional unit testing (i.e., hand writing inputs to the program to test it). The main goal is to automatically generate such tests in order to test behavior in the program (e.g., generate a set of test inputs to have 100% code coverage). The modern versions of these techniques make use of dynamic information (i.e., they actually execute the program under test), and use this information to make decisions about future executions. More concretely, you can imagine the program executing past some branch `if (c)` which was not taken (i.e., `c == false`) and then, the analysis asks the question: "what do the program inputs need to be such that `c == true`. An answer to this question generates new inputs and allows another test to be generated and explored.

Stateless model checking is another automated dynamic technique [7,8,9] used to explore non-determinism in concurrent programs. Essentially, it automatically generates "test cases" (i.e., new thread schedules) to efficiently explore the state space caused by a non-deterministic scheduler.

And there's a bunch of other techniques out there too (e.g., symbolic model checking). There's also a huge amount of work on practical test input generation for hardware. On top of all these techniques, there are there applications to solving specific problems, and heuristics to make them more practical and scalable. Overall, most of the techniques are niche and not widely used, but have been applied in various areas.

[1] https://www7.in.tum.de/~gleissen/papers/sharpie.pdf

[2] http://www.cprover.org/cbmc/

[3] http://www.astree.ens.fr/

[4] https://klee.github.io/

[5] https://www.microsoft.com/en-us/research/project/pex-and-mol...

[6] https://www.visualstudio.com/vs/release-notes/#Testing

[7] https://github.com/markus-kusano/SysTest

[8] http://www.srl.inf.ethz.ch/papers/oopsla15-modelchecking.pdf

[9] http://plrg.eecs.uci.edu/software_page/42-2/

Yes for their microcontrollers they use VxWorks. But Linux is still used for the flight software (i.e. mission control).