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