logoalt Hacker News

joshvmtoday at 3:49 AM0 repliesview on HN

RTOS doesn't give any guarantees about "safe to compute/execute" - that's more the domain of formal verification. In the sense that you can make guarantees about how the program will behave given some domain of inputs. But predictable (or bounded) latency, yes.

You might execute formally verified code within an RTOS, which is your two worlds? Consider you have some critical control loop, like an autopilot (see Ardupilot). That control loop must run at some minimum rate, and the action of the system must be well characterized. Similarly you might want to guarantee that you sample a bunch of sensors frequently enough (so the most recent reading is no older than some time period).