Курс "Методы анализа и обеспечения качества ПО"

2014 учебный год

Лекторы:

• Моисеев М.Ю.
• Ахин М.Х.
• Карпенко А.В.
• Беляев М.А.

Программа курса

Лекции

1. Качество ПО
2. Основы тестирования ПО
3. Полнота тестирования ПО
4. Регрессионное тестирование. Случайное тестирование
5. Отладка ПО
6. Статический анализ
7. Статический анализ параллельных программ
8. Метод проверки моделей. Логика LTL.
9. Метод проверки моделей. Снижение ресурсоемкости.
10. Дедуктивная верификация
11. Методы оценки надежности ПО
    

Вопросы к экзамену

Качество ПО

1. Качество ПО. Модель качества. Задачи обеспечения качества.
2. Классификация методов анализа ПО. Ошибки в программах и их последствия.
3. Классификация ошибок в ПО. Особенности ошибок в параллельных программах.

Тестирование

1. Основы тестирования ПО.
2. Проблема тестовых входных данных.
3. Проблема наблюдаемости.
4. Проблема <<останова>>.
5. Проблема тестового оракула.
6. Регрессионное тестирование.
7. Случайное тестирование.
8. Отладка ПО.

Статический анализ

1. Виды статического анализа. Показатели эффективности. Возможности обнаружения различных видов дефектов с помощью СА.
2. Модели программы используемые для статического анализа.
3. Алгоритмы анализа потока данных. Правила анализа и пример для одного из алгоритмов.
4. Анализ потока данных с использованием теории решеток. Алгоритмы решения системы уравнений над решеткой.
5. Структура и основные алгоритмы для обнаружения ошибок на основе статического анализа.
6. Способы повышения эффективности статического анализа.
7. Проблемы анализа параллельных программ. Общие подходы к анализу многопоточных программ.
8. Общая структура СА многопоточных программ. Основные алгоритмы.

Проверка моделей

1. Определение Модели Крипке. Построение автомата Бюхи по заданной модели Крипке.
2. Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика оператора G, U. Примеры путей, на которых выполняется / не выполняется формула.
3. Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика операторов X, F. Примеры путей, на которых выполняется / не выполняется формула.
4. Конечные автоматы над конечными и бесконечными словами. Идея алгоритма проверки модели для LTL.
5. Автомат Бюхи для пересечения языков. Алгоритм проверки пустоты языка, принимаемого автоматом Бюхи.

Лабораторные работы 2014

Обнаружение дефектов методами статического анализа

Верификация параллельных программ на основе проверки моделей

Архив за предыдущие годы

• 2011/2012 год
• 2010/2011 год