PikeOS
リアルタイムOSとハイパーバイザーを1つのカーネルにまとめたもの。安全重視のソフトウェアと一般のソフトウェアが、互いに干渉せず1つのプロセッサを共有できるように作られている。
PikeOSはドイツのSYSGO社の製品で、同社は2012年にThalesに買収された。カーネルはL4マイクロカーネルの流れをくむ分離カーネルで、自分ではほとんど何もしない代わりに、メモリと時間の両面でパーティションを隔離する。各パーティションはそれぞれの「パーソナリティ」、つまりARINC 653 API、POSIX、Linuxゲスト、別のRTOSなどを動かす。
要点は認証にある。Linux一式にバグがないことの証明は不可能だが、それが隣のパーティションに触れられないことの証明なら現実的だ。PikeOSは航空向けのDO-178C、鉄道向けのEN 50128、自動車向けのISO 26262などの認証を持ち、アビオニクス、鉄道、防衛システムで動いている。