Modeling the Behavior of Threads in the PREEMPT_RT Linux Kernel Using Automata