Environment Modeling of Linux Operating System Device Drivers

• Main Authors: I. S. Zakharov, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov
• Format: Article
• Language: English
• Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
• Series: Труды Института системного программирования РАН
• Subjects: операционная система; драйвер; окружение; верификация
• Online Access: https://ispranproceedings.elpub.ru/jour/article/view/875

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.