Abstract
A formal model of the block-device subsystem of the Linux operating system kernel is set out here, as an introduction to the kernel for formal methods people and a preliminary to further formal methods work. The model is abstract, but executable, and it is faithful to the detail of the real Linux kernel code. The model is used here to analyse kernel behavior. It is proved of the model that the kernel block device system cannot deadlock. © Springer-Verlag 2003.
Cite
CITATION STYLE
Breuer, P. T. (2003). A formal model for the block device subsystem of the Linux kernel. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2885, 599–619. https://doi.org/10.1007/978-3-540-39893-6_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
