Wow, I had no idea. Since their source is closed and untouchable I had no way to check either. Is there any reason there aren't several certified open RTOSes around?
I don't know if there aren't any open certified RTOS's around, but I can explain the 'why' part easily: if you pay for the certification of an open RTOS then everybody that can use one will say 'thank you' for the effort and that's that, since the certification would apply to any and all copies of that particular version. So you're essentially paying for the privilege of cutting your competitors a break.
This could only work if the entity paying for the certification had a way of making that money back somehow and I don't see how that could be done.
Not to detract from the fine work done by the sel4 folks, but there is a large gap between what they have and what DO178 C requires for level A software. Like many other bureaucratic organisations, the FAA (and other regional equivalents) have a process with it's own set of rules (MCDC testing, requirements/design traceability artifacts, etc).
It would cost a significant amount of money to develop the necessary artifacts and engage the FAA to obtain a certification.
That's absolutely true but something like this could be a good starting point.
What I think the whole thread above misses is that the economics simply aren't there, cost isn't the limiting factor for the OS licenses for avionics but an extra certification track (especially for a fast moving target) would be, besides, it is not just the OS that gets certified but you will also have to (separately) certify (usually) the hardware that it runs on (unless you're going to use a design that has already been certified).
That means that modifications are expensive and that 'known to be good' trumps 'could be better' or 'could be cheaper in the longer term'.
Someone would have to come up with a very good reason to see open source trump the existing closed source solutions.
In theory, while certification would be done on a binary derived from seL4, any improvements resulting from the certification process could benefit the open-source core and derivative binaries. Compared to a proprietary OS, improvements would have ecosystem-wide benefits.
In addition, a modular microkernel architecture could use reproducible builds to generate identical binaries from identical source. This would enable binary components to be certified both separately (akin to unit testing) and as an integrated system (mix and match components). This could reduce overall duplication and certification costs, even among competing commercial products derived from seL4 components.
