3 ms·

It's been ~a decade since I was knowledgeable in SpaceX software development details, but at least then, they were not the kind of shop that emphasized rigor an

It's been ~a decade since I was knowledgeable in SpaceX software development details, but at least then, they were not the kind of shop that emphasized rigor and formality. Their culture is oriented toward rapid implementation & test, pragmatism, and empiricism. That has its pluses and minuses. My personal view is that more of the industry, including SpaceX, should be moving toward engineering things to be more correct-by-construction, including formal modeling & verification as you mention. As one example, I don't hear most aerospace firms talking about SeL4 for their flight computer RTOSes. For another, you might be surprised (frightened?) by how many vehicles implement their flight software as big single address space executables written in C (sometimes C++) despite running on modern superscalar processors with MMUs. Even static analysis in some of these codebases is relatively recent - they are heavily dependent on functional testing for safety.

timClicks 5y ago
SeL4 is now mostly defunct. The whole team was laid off during a pivot towards AI and blockchain.
- V_Terranova_Jr 5y ago
  - I don't think SeL4 is "defunct" even though CSIRO's decision on the Trustworthy Systems group was profoundly incompetent; here's a relatively recent post from Gernot Heiser: https://microkerneldude.org/2021/09/28/where-is-sel4-heading/ https://microkerneldude.org/2021/09/28/where-is-sel4-heading... Also: https://sel4.systems/news/2021 https://sel4.systems/news/2021 Do you know more that would substantiate defunct-ness? - Your comment also reinforces my point: if aerospace seeks to be more rigorous, then more in aerospace should be figuring out how to shore up development of SeL4. Instead, they continue with no vision as to what should one day replace things like VxWorks.
sam_bristow 5y ago
Are the properties that have been proven for seL4 particularly relevant for avionics systems? I thought they mainly focussed on process isolation and security. A flight computer would be much more concerned about deterministic performance and real-time guarantees.

timClicks 5y ago

SeL4 is now mostly defunct. The whole team was laid off during a pivot towards AI and blockchain.

V_Terranova_Jr 5y ago
- I don't think SeL4 is "defunct" even though CSIRO's decision on the Trustworthy Systems group was profoundly incompetent; here's a relatively recent post from Gernot Heiser: https://microkerneldude.org/2021/09/28/where-is-sel4-heading/ https://microkerneldude.org/2021/09/28/where-is-sel4-heading... Also: https://sel4.systems/news/2021 https://sel4.systems/news/2021 Do you know more that would substantiate defunct-ness? - Your comment also reinforces my point: if aerospace seeks to be more rigorous, then more in aerospace should be figuring out how to shore up development of SeL4. Instead, they continue with no vision as to what should one day replace things like VxWorks.

sam_bristow 5y ago

Are the properties that have been proven for seL4 particularly relevant for avionics systems? I thought they mainly focussed on process isolation and security. A flight computer would be much more concerned about deterministic performance and real-time guarantees.