Environment Modeling of Linux Operating System Device Drivers
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 so...
| Main Authors: | , , , |
|---|---|
| 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 |
| Summary: | 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. |
|---|---|
| ISSN: | 2079-8156 2220-6426 |