To specify the design of operating systems and other “systems level” software, it’s possible to use temporal-logic style qualifiers like “always” or “eventually” or more detailed similar qualifiers in just ordinary algebra and state machines. https://www.yodaiken.com/wp-content/uploads/2025/10/temporal.pdf
Real-time operating systems are either a solved problem or a backwater of engineering design. Threads, semaphores, mutexes, some basic I/O, priority scheduling all of this has been more or less standardized in the POSIX 1003.13 smaller profiles (51,52) for many
If anything, Wind River’s inability to breakout, despite a once Microsoft-like position of dominance, is a by-product of their failure to meaningfully go “up the stack” and away from their historical focus on the silicon layer as a primary differentiation
This paper by Prof. Edward Lee explains something of why “threads” are such a painful abstraction. As Prof. Lee notes, threads intrinsically create unspecified program operation (which he calls non-determinism) and resource conflicts which we then attempt to “prune” via