[SystemSafety] C for OSs

[Roderick Chapman]

On 06/09/2019 16:17, Martyn Thomas wrote:

> SFAIK, the iFACTS air traffic control tools were written in SPARK and
> run on the bare hardware.

No... iFACTS runs on the same infrastructure as NERC, which is IBM 
hardware running AIX (albeit a _very_ stable and well-controlled release 
of AIX). For SPARK, this is something of an oddity, since most SPARK 
system do indeed run bare-metal or on some sort of small RTOS.

The Muen hypervisor is an interesting an example - an entire x86_64 
hypervisor, that is written in SPARK, and has been subject to proofs of 
type-safety and so on.  It's open source and here

  https://muen.codelabs.ch

  - Rod