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.
Automata-based modeling of interrupts in the Linux PREEMPT RT kernel
Cucinotta, Tommaso;Abeni, Luca
2017-01-01
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.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
ETFA-2017.pdf
accesso aperto
Tipologia:
Documento in Post-print/Accepted manuscript
Licenza:
PUBBLICO - Pubblico con Copyright
Dimensione
325.76 kB
Formato
Adobe PDF
|
325.76 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.