A mechanism for verifying the correct operation of the kernel has been proposed for Linux.
A set of patches implementing the RV (Runtime Verification) mechanism is proposed for inclusion in Linux kernel 5.20 (possibly the branch will be numbered 6.0). This mechanism provides tools for verifying the correctness of operation in highly reliable systems, ensuring the absence of failures. Verification is performed at runtime by attaching handlers to trace points that compare the actual execution path with a previously defined reference deterministic model of the automaton, […]
