I’ve been working with the application of formal methods on Linux since my Ph.D. The idea was to formally model the behavior of threads on the PREEMPT RT Linux kernel, and then use the model to perform the runtime verification and timing analysis of the threads.
My research is divided into three stages:
In the Linux Task Model page, you can find mode about modeling part of the Linux Behavior
In the Efficient Formal Verification for the Linux Kernel page, you can find more about the runtime monitoring of automata-based models for Linux.
In the Demystifying the Real-Time Linux Scheduling Latency page, you can find more about the timing analysis of the PREEMPT_RT.
The results of this research is compiled on my thesis, which is here.