Курс "Методы анализа и обеспечения качества ПО"
2011/2012 учебный год
Лекторы:
- Моисеев М.Ю.
- Ахин М.Х.
- Захаров А.В.
- Цесько В.А.
- Карпенко А.В.
- Беляев М.А.
Программа курса
Лекции
- Качество ПО. Вводная лекция
- Основы тестирования
- Полнота тестирования: оценка и обеспечение
- Тестирование и жизненный цикл ПО
- Введение в статический анализ ПО
- Обнаружение программных ошибок методами статического анализа
- Системы типов и эффектов
- Введение в верификацию на основе проверки модели
- Метод проверки модели. Методы снижения размерности задачи
- Построение моделей программ с помощью SAT-solvers
- Математический аппарат дедуктивной верификации ПО
- Обзор методов оценки качества ПО
- Изоморфизм Карри-Говарда
Лабораторные работы
- Тестирование ПО
- Современные средства статического анализа программ (MS SCA, Aegis)
- Применение систем типов для анализа ПО (Coq)
- Верификация ПО на основе проверки моделей (SPIN)
- Верификация программ с помощью SAT solvers (SatAbs)
- Дедуктивная верификация (Frama-C)
Вопросы к экзамену
Качество ПО
- Качество ПО. Модель качества. Задачи обеспечения качества.
- Методы анализа ПО. Ошибки в программах и их последствия.
Тестирование
- Цель тестирования ПО. Обобщенная схема проведения тестирования ПО. Модель программной ошибки. Уровни тестирования ПО.
- Модульное тестирование ПО. Виды модульного тестирования.
- Интеграционное тестирование ПО. Виды интеграционного тестирования. Системное тестирование ПО.
- Полнота тестирования ПО. Виды тестового покрытия.
- Покрытие потока управления. Покрытие потока данных.
- Мутационное тестирование ПО. Design for Testability.
- Способы обеспечения управляемости. Способы обеспечения наблюдаемости.
- Регрессионное тестирование ПО. Виды выборочного регрессионного тестирования.
- Управление регрессионными тестами.
Статический анализ
- Виды статического анализа. Показатели эффективности. Анализа потока управления.
- Алгоритмы анализа потока данных. Правила анализа и пример для одного из алгоритмов.
- Анализ потока данных с использованием теории решеток. Алгоритмы решения системы уравнений над решеткой.
- Классификация программных ошибок.
- Модели программы используемые для статического анализа.
- Структура и основные алгоритмы для обнаружения ошибок на основе статического анализа.
- Системы типов как вид статического анализа. Формализм. Type soundness и type completeness. Алгоритмы и способы вывода.
- Системы типов как вид статического анализа. Отношения частичного порядка. Проблемы применения СТ к императивным языкам.
- Системы типов как вид статического анализа. Системы типов и эффектов. Предпосылки, основная идея. Дальнейшее увеличение сложности и возможные проблемы.
Проверка моделей
- Определение Модели Крипке. Построение автомата Бюхи по заданной модели Крипке.
- Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика оператора G, U. Примеры путей, на которых выполняется / не выполняется формула.
- Линейная темпоральная логика. Структура формул. Синтаксис. Пути. Семантика операторов X, F. Примеры путей, на которых выполняется / не выполняется формула.
- Конечные автоматы над конечными и бесконечными словами. Идея алгоритма проверки модели для LTL.
- Автомат Бюхи для пересечения языков. Пример.
- Алгоритм проверки пустоты языка, принимаемого автоматом Бюхи. Идея верификации на-лету.
- Проблема экспоненциального роста пространства состояний. Методы снижения размерности пространства состояний. Абстракция данных, абстракция предикатов, SatAbs.
- Проблема экспоненциального роста пространства состояний. Методы снижения размерности пространства состояний. Бинарные решающие диаграммы, редукция частичных порядков.
- Проблема экспоненциального роста пространства состояний. Методы снижения размерности пространства состояний. Слайсинг.
Дедуктивная верификация
- Определение дедуктивной верификации. Виды программ. Виды ошибок. Место среди других методов. Достоинства и недостатки.
- Логики различных порядков. Синтаксис и семантика термов. Присваивания.
- Синтаксис и семантика формул. Подстановки. Модель, тавтология и противоречие.
- Выразительность логик. Пропозициональная логика.
- Доказательство теорем. Системы доказательств. Аксиомы и правила вывода. Forward reasoning. Backward reasoning.
- Свойства систем доказательств: корректность, полнота, разрешимость, структурная полнота. Пропозициональная логика.
- Верификация блок-схем алгоритмов. Частичная корректность.
- Верификация блок-схем алгоритмов. Полная корректность и завершаемость.
Методы оценки качества ПО
- Методы оценки надежности ПО. Динамические методы. Модели роста надежности.
- Методы оценки надежности ПО. Статические методы. Модели сложности.