Main page Research activities Publications Talks MSc thesis projects Hobby and spare time Write me This site uses
Google Analytics
Last updated on
17 June 2017

Publication details

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.

Abstract

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.

Download paper


Main page Research activities Publications Talks MSc thesis projects Hobby and spare time Write me Last updated on