Захаров Илья Сергеевич Методы декомпозиции систем и моделирования окружения программных модулей для верификации Си-программ

Краткое описание

Захаров Илья Сергеевич Методы декомпозиции систем и моделирования окружения программных модулей для верификации Си-программ
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Захаров Илья Сергеевич
Введение

Глава 1. Обзор работ в области верификации моделей программных систем на языке Си

1.1. Верификация моделей Си-программ

1.2. Инструменты верификации моделей Си-программ

1.3. Ограничения подходов к применению инструментов верификации моделей Си-программ

1.4. Методы распараллеливания верификации моделей программ

1.5. Требования к системе верификации моделей крупных программных систем на языке Си

Глава 2. Подготовка верификационных задач

2.1. Программный интерфейс модулей Си-программ

2.2. Схема генерации верификационных задач

2.3. Метод декомпозиции Си-программ на модули

2.4. Метод спецификации моделей окружения

2.5. Метод синтеза моделей окружения

2.6. Синтез моделей требований

2.7. Компоновка верификационных задач

Глава 3. Архитектура системы верификации

3.1. Компоненты системы верификации

3.2. Сервер

3.3. Генератор верификационных задач

3.4. Решатель верификационных задач и заданий

Глава 4. Реализация методов

4.1. Сервер

4.2. Генератор верификационных задач

4.3. Решатель верификационных задач и заданий

Глава 5. Результаты практического применения

5.1. Критерии оценки результатов

5.2. Верификация ОС Linux

5.3. Верификация апплетов проекта BusyBox

5.4. Область применимости и ограничения метода

Заключение

Публикации автора по теме диссертации

Цитированная литература

Введение