Автоматизированный контроль корректности MPI-программ на основе шаблонов ошибочного поведения

• Автор: Власенко, Андрей Юрьевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2014
• Место защиты: Кемерово
• Количество страниц: 193 с. : ил.

Оглавление
Оглавление
Введение
ГЛАВА 1. СЕМАНТИЧЕСКИЕ ОШИБКИ В ПАРАЛЛЕЛЬНЫХ ПРОГРАММАХ И ПОДХОДЫ К ИХ ОБНАРУЖЕНИЮ
1.1 Семантические ошибки в параллельных программах
1.2 Опрос пользователей
1.3 Методы и программные средства обнаружения семантических ошибок
1.3.1 Диалоговая отладка
1.3.2 Верификация модели программы
1.3.3 Сравнительная отладка
1.3.4 Автоматизированный анализ корректности
1.3.5 Анализ по трассе
1.3.6 Анализ во время исполнения
ГЛАВА 2. ШАБЛОНЫ ОШИБОЧНОГО ПОВЕДЕНИЯ
2.1 Система описания шаблонов ошибочного поведения
2.2 Примеры шаблонов
2.2.1 Шаблоны для локальных ошибок
2.2.2 Шаблоны для глобальных ошибок
ГЛАВА 3. МОДЕЛЬ И АЛГОРИТМЫ ОБНАРУЖЕНИЯ
СЕМАНТИЧЕСКИХ ОШИБОК СИСТЕМОЙ
АВТОМАТИЗИРОВАННОГО КОНТРОЛЯ КОРРЕКТНОСТИ
3.1 Требования к системе автоматизированного контроля корректности. Анализ требований

3.2 Моделирование поведения системы автоматизированного контроля корректности
3.3 Архитектура и основные структуры данных
3.3.1 Конфигурационный файл
3.3.2 Утилита запуска
3.3.3 Препроцессор
3.3.4 МРКпроцессы
3.3.5 Сервер-анализатор
3.4 Процесс выявления соответствия поведения МР1-программы шаблонам ошибочного поведения
ГЛАВА 4. ТЕСТИРОВАНИЕ СИСТЕМЫ АВТОМАТИЗИРОВАННОГО КОНТРОЛЯ КОРРЕКТНОСТИ. ПРИМЕРЫ АНАЛИЗА ПРОГРАММ
4.1 Тестовая база
4.2 Используемые тесты
4.3 Анализ проведенных тестов
4.4 Отладка прикладных МР1-программ
Заключение
Список литературы
Приложение 1. Определение системы описания шаблонов в расширенной форме Бэкуса-Наура
Приложение 2. МР1-программа сортировки массива методом чет-нечетной перестановки
Приложение 3. МРЬпрограмма поблочного умножения матрицы на вектор
Приложение 4. Текст шаблонов для распространенных ошибок МР1-программ
Приложение 5. Свидетельство о регистрации разработанного программного средства
Приложение 6. Акт о внедрении программного средства

Суть метода заключается в следующем. Для заданной анализируемой программы строится ее абстрактная формальная модель. Чаще всего она представляется в виде системы переходов между состояниями. В качестве состояния выступает кортеж значений переменных, фигурирующих в программе, а в качестве перехода между состояниями, соответственно, изменение переменной своего значения. Затем производится спецификация свойств, которыми должна обладать система. Например, желательно показать, что некоторая параллельная программа никогда не попадает в тупик (не образуется дедлок). Чтобы модель была пригодна для верификации, в ней должны проявляться те свойства, анализ которых необходим для установления ее корректности. С другой стороны, она должна быть свободна от частных особенностей, не влияющих на проверяемые свойства, но усложняющих верификацию. Проверяемые свойства или требования выражаются на формальном математическом языке (например, представляются в виде логических формул). После этого верификация программы сводится к проверке выполнимости формализованного требования (спецификации) на абстрактной модели. При этом ведется перебор возможных состояний по разным маршрутам в графе. Если результаты проверки отрицательные, то пользователю предоставляют трассу, содержащую ошибку. Она строится в качестве контрпримера для проверяемого свойства и помогает проектировщику проследить, где возникает ошибка. Анализ ошибочной трассы может повлечь за собой модификацию системы и повторное применение алгоритма проверки на модели.
Главным плюсом такого подхода является то, что решается одна из основных проблем предыдущего класса инструментальных средств отладки- большая сложность обнаружения потенциальных ошибок, возникающих из-за недетерминированного поведения параллельной программы. Каждый раз при запуске приложения под управлением диалогового отладчика оно проходит лишь один из возможных маршрутов в графе состояния и проблемы, которые могут появиться на других маршрутах остаются «в тени». Основная же трудность, которую при-