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

2011/2012 учебный год

Лекторы:

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

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

Лекции

1. Качество ПО. Вводная лекция
2. Основы тестирования
3. Полнота тестирования: оценка и обеспечение
4. Тестирование и жизненный цикл ПО
5. Введение в статический анализ ПО
6. Обнаружение программных ошибок методами статического анализа
7. Системы типов и эффектов
8. Введение в верификацию на основе проверки модели
9. Метод проверки модели. Методы снижения размерности задачи
10. Построение моделей программ с помощью SAT-solvers
11. Математический аппарат дедуктивной верификации ПО
12. Обзор методов оценки качества ПО
13. Изоморфизм Карри-Говарда

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

1. Тестирование ПО
2. Современные средства статического анализа программ (MS SCA, Aegis)
3. Применение систем типов для анализа ПО (Coq)
4. Верификация ПО на основе проверки моделей (SPIN)
5. Верификация программ с помощью SAT solvers (SatAbs)
6. Дедуктивная верификация (Frama-C)

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

Качество ПО

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

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

1. Цель тестирования ПО. Обобщенная схема проведения тестирования ПО. Модель программной ошибки. Уровни тестирования ПО.
2. Модульное тестирование ПО. Виды модульного тестирования.
3. Интеграционное тестирование ПО. Виды интеграционного тестирования. Системное тестирование ПО.
4. Полнота тестирования ПО. Виды тестового покрытия.
5. Покрытие потока управления. Покрытие потока данных.
6. Мутационное тестирование ПО. Design for Testability.
7. Способы обеспечения управляемости. Способы обеспечения наблюдаемости.
8. Регрессионное тестирование ПО. Виды выборочного регрессионного тестирования.
9. Управление регрессионными тестами.

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

1. Виды статического анализа. Показатели эффективности. Анализа потока управления.
2. Алгоритмы анализа потока данных. Правила анализа и пример для одного из алгоритмов.
3. Анализ потока данных с использованием теории решеток. Алгоритмы решения системы уравнений над решеткой.
4. Классификация программных ошибок.
5. Модели программы используемые для статического анализа.
6. Структура и основные алгоритмы для обнаружения ошибок на основе статического анализа.
7. Системы типов как вид статического анализа. Формализм. Type soundness и type completeness. Алгоритмы и способы вывода.
8. Системы типов как вид статического анализа. Отношения частичного порядка. Проблемы применения СТ к императивным языкам.
9. Системы типов как вид статического анализа. Системы типов и эффектов. Предпосылки, основная идея. Дальнейшее увеличение сложности и возможные проблемы.

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

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

Дедуктивная верификация

1. Определение дедуктивной верификации. Виды программ. Виды ошибок. Место среди других методов. Достоинства и недостатки.
2. Логики различных порядков. Синтаксис и семантика термов. Присваивания.
3. Синтаксис и семантика формул. Подстановки. Модель, тавтология и противоречие.
4. Выразительность логик. Пропозициональная логика.
5. Доказательство теорем. Системы доказательств. Аксиомы и правила вывода. Forward reasoning. Backward reasoning.
6. Свойства систем доказательств: корректность, полнота, разрешимость, структурная полнота. Пропозициональная логика.
7. Верификация блок-схем алгоритмов. Частичная корректность.
8. Верификация блок-схем алгоритмов. Полная корректность и завершаемость.

Методы оценки качества ПО

1. Методы оценки надежности ПО. Динамические методы. Модели роста надежности.
2. Методы оценки надежности ПО. Статические методы. Модели сложности.

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

• 2010/2011 год