Red Hat Research’s Dr. Daniel Bristot de Oliveira continues to deliver practical improvements to the Linux kernel, this time with the addition of the Runtime Verification subsystem to the Linux kernel 6.0.
Daniel has been exploring methods to improve the analysis of the real-time properties of Linux over the past ten years. His research explores the tracing features of Linux to derive fine-grained properties of the kernel, overcoming a known limitation of the usage of black-box testing by developers while increasing confidence in Linux usage on safety-critical real-time systems. In May 2022, Red Hat Research shared news of Daniel’s contribution of the Real-Time Linux Analysis toolset (RTLA) as of the Linux 5.17 release.
Daniel’s research has been featured in RHRQ in October 2020, February 2021, and May 2021.
Runtime Verification (RV) is a rigorous method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems. RV works by analyzing the trace of the system’s actual execution, comparing it against a formal specification of the system behavior. The main advantage is that RV can give precise information on the runtime behavior of the monitored system without the pitfalls of developing models that require a re-implementation of the entire system in a modeling language.
Moreover, given an efficient monitoring method, it is possible to execute an online verification of a system, enabling the reaction for unexpected events and avoiding, for example, the propagation of a failure on safety-critical systems. Such verification tools are becoming essential to the development of Linux for safety-critical systems, targeting, for example, automotive and industrial applications.
The initial support for RV includes online monitors in the Linux kernel, but RV was designed with extensibility in mind. It is expected to be extended with other theoretical analysis tools, serving as the starting point for researchers and practitioners to develop other verification methods. Red Hat Research’s Dr. Daniel is the maintainer of RV in the Linux kernel and actively participates in the academic community, helping to fill the gap between theory and practice with collaboration from both communities.
Watch the Red Hat Research website for more theoretical and practical developments on runtime verification-related topics.
About Daniel
Daniel has a joint PhD in Automation Engineering from Universidade Federal de Santa Catarina (Brazil) and Embedded Real-Time systems from Scuola Superiore Sant’Anna (Italy). Currently, he is a Senior Principal Software Engineer at Red Hat, working on developing the real-time features of the Linux kernel. Daniel helps in the maintenance of real-time related tracers and toolings for the Linux kernel and the SCHED_DEADLINE. He is an affiliate researcher at the Retis Lab and researches real-time and formal methods. He is an active member of the real-time academic community, participating in the technical program committee of academic conferences, such as the Real-Time Systems Symposium, the Real-Time Technology and Applications Symposium, and the Euromicro Conference on Real-Time Systems.
