|
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This site uses |
Last updated on
22 February 2025 |
D. B. de Oliveira, R. S. de Oliveira, T. Cucinotta, L. Abeni. "Automata-Based Modeling of Interrupts in the Linux PREEMPT RT Kernel," in Proceedings of the 22nd IEEE International Conference on Emerging Technologies And Factory Automation (ETFA 2017), September 12-15, 2017, Limassol, Cyprus.
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.
Copyright by IEEE.
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Last updated on
22 February 2025 |