Ви є тут

Верификация драйверов операционной системы Linux при помощи предикатных абстракций

Автор: 
Мутилин Вадим Сергеевич
Тип роботи: 
Кандидатская
Рік: 
2012
Артикул:
336327
179 грн
Додати в кошик

Вміст

Содержание
Введение .
Глава 1. Обзор работ в области верификации драйверов операционных систем.
1.1. Ядро ОС Ьпих
1.2. Правила .
1.3. Инструменты тестирования динамической верификации .
1.4. Общецелевые инструменты статического анализа .
1.5. Системы верификации драйверов операционных систем
1.6. Выводы.
Глава 2. Метод верификации драйверов ОС Ьпих
2.1. Поток команд
2.2. Шаг 1
2.3. Шаг 2
2.4. Шаг 3
2.5. Построение моделей правил .
2.6. Отделение привязки к интерфейсу ядра .
Глава 3. Метод генерации окружения целевого драйвера .
3.1. Сценарии взаимодействия .
3.2. Основные определения
3.3. Формальная модель драйвера и его окружения в 7гисчислении
3.4. Примеры задания окружения в виде процессов с учетом правил взаимодействия
3.5. Трансляция процессов в Си программу
Глава 4. Методы оптимизации анализа при помощи предикатных абстракций.
4.1. Общая информация.
4.2. Метод СЕСАЛ
4.3. Известные ограничения
4.4. Выводы.
Глава 5. Система верификации драйверов ОС Ыпих.
5.1. Пользовательский интерфейс системы
5.2. Разработка адаптера инструмен та верификации.
Глава 6. Методика выявления и классификации правил корректности .
6.1. Выбор источника .
6.2. Методика анализа журнала изменений
6.3. Классификация ошибок взаимодействия драйверов с ядром
ОС Ьших.
6.4. Аналогичные работы .
Глава 7. Практические результаты .
Заключение .
Литература