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.
2017
978-1-5090-6505-9
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11382/519625
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
social impact