A Correction

A Correction

Last modified 12 November 2016
In several talks I gave in 2015 and 2016, I said that the Virtuoso real time operating system [RTOS] that flew on the European Space Agency's Rosetta spacecraft was designed using TLA+.  That was not correct.  TLA+ was used to design OpenComRTOS, a successor to Virtuoso.  I beileve that everything I said about the benefits of using TLA+ apply to OpenComRTOS--including that its code size was 10 times smaller than that of the previous version.  However, it was the previous version, Virtuoso, that flew on Rosetta.

I am very sorry about this mistake.

Leslie Lamport