Курс "Методы анализа и обеспечения качества ПО"
2014 учебный год
Лекторы:
- Моисеев М.Ю.
- Ахин М.Х.
- Карпенко А.В.
- Беляев М.А.
Программа курса
Лекции
- Качество ПО
- Основы тестирования ПО
- Полнота тестирования ПО
- Регрессионное тестирование. Случайное тестирование
- Отладка ПО
- Статический анализ
- Статический анализ параллельных программ
- Метод проверки моделей. Логика LTL.
- Метод проверки моделей. Снижение ресурсоемкости.
- Дедуктивная верификация
- Методы оценки надежности ПО
Вопросы к экзамену
Качество ПО
- Качество ПО. Модель качества. Задачи обеспечения качества.
- Классификация методов анализа ПО. Ошибки в программах и их последствия.
- Классификация ошибок в ПО. Особенности ошибок в параллельных программах.
Тестирование
- Основы тестирования ПО.
- Проблема тестовых входных данных.
- Проблема наблюдаемости.
- Проблема <<останова>>.
- Проблема тестового оракула.
- Регрессионное тестирование.
- Случайное тестирование.
- Отладка ПО.
Статический анализ
- Виды статического анализа. Показатели эффективности. Возможности обнаружения различных видов дефектов с помощью СА.
- Модели программы используемые для статического анализа.
- Алгоритмы анализа потока данных. Правила анализа и пример для одного из алгоритмов.
- Анализ потока данных с использованием теории решеток. Алгоритмы решения системы уравнений над решеткой.
- Структура и основные алгоритмы для обнаружения ошибок на основе статического анализа.
- Способы повышения эффективности статического анализа.
- Проблемы анализа параллельных программ. Общие подходы к анализу многопоточных программ.
- Общая структура СА многопоточных программ. Основные алгоритмы.
Проверка моделей
- Определение Модели Крипке. Построение автомата Бюхи по заданной модели Крипке.
- Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика оператора G, U. Примеры путей, на которых выполняется / не выполняется формула.
- Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика операторов X, F. Примеры путей, на которых выполняется / не выполняется формула.
- Конечные автоматы над конечными и бесконечными словами. Идея алгоритма проверки модели для LTL.
- Автомат Бюхи для пересечения языков. Алгоритм проверки пустоты языка, принимаемого автоматом Бюхи.
Верификация параллельных программ на основе проверки моделей