To be included in the Linux 5.20 kernel (perhaps the branch will be numbered 6.0), a set of patches has been proposed with the implementation of the RV (Runtime Verification) mechanism, which is a means for checking the correct operation on highly reliable systems that guarantee the absence of failures. Validation is done at runtime by attaching handlers to tracepoints that check the actual progress of execution against a predetermined reference deterministic model of the automaton that determines the expected behavior of the system.
Information from tracepoints moves the model from one state to another, and if the new state does not match the parameters of the model, a warning is generated or the kernel is put into a "panic" state (it is understood that highly reliable systems will detect such situations and respond to them). The automaton model that defines transitions from one state to another is exported to the βdotβ (graphviz) format, after which it is translated using the dot2c utility into a C representation, which is loaded in the form of a kernel module that tracks deviations of the execution progress from a predefined model.
Run-time model checking is positioned as a more lightweight and easy-to-implement method of verifying the correctness of execution on mission-critical systems, complementing classical methods of reliability verification, such as model checking and mathematical proofs of code compliance with specifications given in a formal language. Among the advantages of RV is the ability to provide rigorous verification without a separate implementation of the entire system in a modeling language, as well as a flexible response to unforeseen events, for example, to block further propagation of a failure in critical systems.
Source: opennet.ru