Generating Environment Model for Linux Device Drivers.

Generating Environment Model for Linux Device Drivers.

Авторы

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

Аннотация

Linux device drivers can't be analyzed separately from the kernel core due to their large interdependency with each other. But source code of the whole Linux kernel is rather complex and huge to be analyzed by existing model checking tools. So a driver should be analyzed with environment model instead of the real kernel core. In the given paper requirements for driver environment model are discussed. The paper describes advantages and drawbacks of existing model generating approaches used in different systems of model checking device drivers. Besides, the paper presents a new method for generating model for Linux device drivers. Its features and shortcomings are demonstrated on the basis of application results.

Ключевые слова

operating system, Linux, kernel, driver, model checking, environment model, Pi-processes.

Издание

Proceedings of the 7th Spring/Summer Young Researchers' Colloquium on Software Engineering. Kazan. 2013.

ISBN 978-5-91474-020-4.

Научная группа

Технологии программирования

Все публикации за 2013 год

Все публикации