Формальные методы верификации и тестирования телекоммуникационных протоколов и сервисов

Магистратура 2021/2022

Статус: Курс обязательный (Системное программирование)

Направление: 09.04.04. Программная инженерия

Кто читает: Базовая кафедра «Системное программирование» Института системного программирования им. В.П. Иванникова РАН (ИСП РАН)

Где читается: Факультет компьютерных наук

Когда читается: 2-й курс, 1, 2 модуль

Формат изучения: без онлайн-курса

Охват аудитории: для всех кампусов НИУ ВШЭ

Преподаватели: Евтушенко Нина Владимировна

Прогр. обучения: Системное программирование

Язык: русский

Кредиты: 8

Контактные часы: 44

Полная версия программы учебной дисциплины

Аннотация

Дисциплина «Формальные методы верификации и тестирования телекоммуникационных протоколов и сервисов» направлена на изучение основных принципов использования формальных методов для верификации и тестирования телекоммуникационных протоколов и сервисов, в том числе,для получения навыков анализа телекоммуникационных протоколов и сервисов и их реализаций с использованием формальных методов. В результате освоения дисциплины студент должен знать основные математические модели и методы их анализа, используемые для тестирования и верификации телекоммуникационных протоколов и сервисов; их основные достоинства и недостатки, и уметь применять известные формальные методы при верификации и тестировании телекоммуникационных протоколов и сервисов.

Цель освоения дисциплины

Знание основных математических моделей и методов их анализа, используемых для тестирования и верификации телекоммуникационных протоколов и сервисов; их основные достоинства и недостатки
Умение применять известные формальные методы при верификации и тестировании телекоммуникационных протоколов и сервисов
Владение навыками верификации и тестирования телекоммуникационных протоколов и сервисов на основе формальных моделей

Планируемые результаты обучения

Владеть методами построения проверяющих тестов с гарантированной полнотой на основе классических и неклассических автоматных моделей
Знать подходы к верификации и тестированию криптографических протоколов
Уметь использовать формальные модели для анализа функциональных и нефункциональных свойств сетевых сервисов
Уметь пользоваться верификаторами и решателями (SPIN, z3 и др.) для проверки многокомпонентных программных систем на безопасность, в том числе, на наличие осцилляций и тупиковых ситуаций

Содержание учебной дисциплины

Введение
Использование моделей с конечным числом переходов при тестировании реализаций телекоммуникационных протоколов
Криптографические протоколы
Верификация телекоммунационных протоколов
Использование формальных моделей для анализа функциональных и нефункциональных свойств сетевых сервисов
Использование формальных моделей для анализа компонентов программно-конфигурируемых сетей

Элементы контроля

Выступление с презентацией (ДЗ1)
Подготовка презентации по одной и тем использования формальных подходов к анализу телекоммуникационных протоколов и сервисов
Лабораторная работа (ДЗ2)
Лабораторная работа по умению пользоваться верификатором Spin для проверки элементов протокола OpenFlow
Экзамен (Экз)

Промежуточная аттестация

2021/2022 учебный год 2 модуль
Оценка за первый семестр (итоговая оценка Оитог.1 складывается из накопленной оценки 1 семестра (Онакопл.1) и оценки за устный экзамен в конце 2-го модуля (Оэкз.1): Онакопл.1 = Одом.зад.; Оитог.1= 0.5⋅Онакопл.1 + 0.5⋅Оэкз.1; Оценка (Оитог.1) является результирующей

Программа дисциплины