Читается в весеннем семестре на первом курсе магистратуры МФТИ.
Преподаватель: к.ф.-м.н. Мутилин Вадим Сергеевич.
Цель курса — познакомить с предметом верификации ПО, представить широкую палитру существующих методов и подходов, осветить преимущества и ограничения, присущие методам верификации. В рамках курса рассматриваются общее понятие качества ПО, подпроцессы обеспечения качества в рамках жизненного цикла ПО, методы статического анализа программ, методы проверки моделей, методы динамического анализа программ и различные варианты функционального тестирования.
Задачами данного курса являются:
- формирование базовых знаний в области обеспечения качества ПО, как неотъемлемой части теории и практики разработки ПО, адресуемого к проблемам построения корректных и надежных программ, и имеющего важное методологическое значение как для подготовки специалистов в области современных информационных технологий, так и для поддержки разнообразных инновационных сфер деятельности;
- обучение студентов основам жизненного цикла программного обеспечения и задачам верификации, возникающим в ходе разработки, внедрения и эксплуатации ПО;
- обучение студентов методам функционального тестирования, применяемым в различных сценариях разработки ПО, включая модульное тестирование, случайное тестирование, тестирование с использованием моделей, а также методам оценки полноты тестирования;
- обучение студентов базовым методам анализа корректности программ;
- формирование теоретических подходов к верификации программного обеспечения для проведения исследований в рамках выпускных работ на степень магистра.
Планируемые результаты обучения:
- знать место и роль средств верификации в разработке ПО;
- знать связь курса верификации со смежными дисциплинами дискретной математики и проектирования программных комплексов;
- знать методы тестирования и аналитического исследования ПО;
- знать современные средства и технологии верификации;
- уметь эффективно использовать на практике теоретические знания в области верификации программ;
- уметь представить панораму универсальных и специальных методов верификации;
- уметь выбрать методы и сценарии верификации, адекватные предметной области и исследуемой задаче;
- уметь эффективно применять средства верификации для обеспечения качества разрабатываемого программного обеспечения;
- владеть современными средствами и технологиями верификации ПО;
- владеть навыками использования систем тестирования для языков высокого уровня;
- владеть навыками использования систем динамического исследования программ;
- владеть навыками использования систем аналитического исследования программ.
Рассматриваемые темы:
- Обзор методов верификации.
- Понятие качества ПО.
- Тестирование. Тестовые покрытия.
- Разработка через тестирование. Рефакторинг.
- Статическая верификация программ с использованием проверки моделей.
- Верификация с абстракциями и уточнениями.
- Динамический анализ программ.
- Непрерывная интеграция. Встраивание методов верификации.