Proceedings of ISP RAS

Environment Modeling of Linux Operating System Device Drivers.

I.S. Zakharov, V.S. Mutilin, E.M. Novikov, A.V. Khoroshilov.


To establish verification of Linux operating system device drivers it is necessary to take into account particularity of communication between drivers and a kernel core as far as it plays the main role in drivers behavior. At the same time, verification of a driver together with kernel core source code is not feasible due to complexity and size of the resulting code. That is why we suggest to replace the real environment with its model. Such model of the environment should be correct and complete. Correctness means that it should contain only interaction scenarios which can happen in the real environment. Completeness means that all feasible in the real environment scenarios should present in the corresponding model. Moreover, the environment model should be able to be checked by verification tools. Hence, it should be translated in equivalent representation supported by these tools. The paper presents a new method for modeling driver environment based on R. Milner calculus and a method of model translation into a program in the C programming language. Being linked with driver source code this program describes the same scenarios of driver behavior as the real driver environment in the operating system.


operating system; driver; environment; verification


Proceedings of the Institute for System Programming, vol. 25, 2013, pp. 85-112.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2013-25-6

Full text of the paper in pdf (in Russian) Back to the contents of the volume