This paper presents a methodology to model and check the behavior of a part of the Linux kernel by applying automaton theory and in-kernel tracing from real execution. It is possible to check that the state transitions of the kernel during a real execution match with the allowed ones, according to the formal model. The scope of the paper is limited to the IRQ/NMI subsystem of the Linux kernel.
|Titolo:||Automata-based modeling of interrupts in the Linux PREEMPT RT kernel|
|Data di pubblicazione:||2017|
|Appare nelle tipologie:||4.1 Contributo Atti Congressi/Articoli in extenso|