At the OSPERT'15 workshop, located in Lund, Sweden, the dOSEK team presented an approach to replace the actual kernel implementation with an equivalent state machine. As the result of an abstract simulation of the application logic on top of the operating-system model, we get a state machine that captures the interaction between those two components. Such a state machine might look like this:
The real-time kernel is represented as a state machine, where the states are labeled with symbols. Each state has the currently running task (Idle, T1, or ISR) as an output value. Transitions between states are issued by system-calls, which act as events in our model.
Currently, we are aiming to implement application specific state machines as processor extensions.
