Environment Modeling of Linux Operating System Device Drivers

Abstract

In static device driver verification of Linux operating system it is necessary to take into account the specifics of the communication between drivers and kernel core as far as it plays the main role in the drivers’ behavior. At the same time the verification of a driver together with kernel core source code is not feasible due to complexity and size of the resulting source code. As a solution the paper presents the modeling method of driver environment based on R.Milner  calculus and the method of  model translation into C program. Being linked with the driver the resulting program has the same scenarios of driver behavior as the real driver environment in operating system from the static verification tools point of view.

Keywords

• операционная система
• драйвер
• окружение
• верификация