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

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

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

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

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

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

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

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

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

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

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

Кредиты: 8

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

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

Аннотация

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

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

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

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

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

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

Введение
Использование формальных методов при верификации и тестировании телекоммуникационных протоколов. Эволюция формальных методов и средств и оценки эффективности их использования. Обоснование необходимости использования формальных методов при верификации и тестировании сетевых сервисов.
Использование моделей с конечным числом переходов при тестировании реализаций телекоммуникационных протоколов
Использование моделей с конечным числом переходов при тестировании телекоммуникационных протоколов, в частности, конечных автоматов и полуавтоматов, входо-выходных полуавтоматов (трансдьюсеров), расширенных и временных автоматов и полуавтоматов; использование автоматных моделей с бесконечным числом переходов при символьном тестировании (symbolic testing). Построение проверяющих тестов с гарантированной полнотой на основе классических и неклассических автоматных моделей для тестирования протокольных реализаций; полнота проверяющих тестов.
Криптографические протоколы
Безопасность протокольных реализаций как цепочки «стойкость алгоритма – верификация модели - обнаружение уязвимостей в реализации». Анализ безопасности протокола TLS, в том числе, анализ обнаруженных угроз и уязвимостей в протоколе и, соответственно, в его реализациях.
Верификация телекоммунационных протоколов
Верификация многокомпонентных программных систем с использованием композиций автоматных моделей; использование верификаторов и решателей (SPIN, z3 и др.) при проверке свойств безопасности, в том числе, проверке наличия тупиков и зацикливаний.
Использование формальных моделей для анализа функциональных и нефункциональных свойств сетевых сервисов
Формальные модели для анализа телекоммуникационных сервисов. Использование моделей с конечным числом переходов на различных этапах их жизненного цикла; формальные методы при анализе качества сервиса с точки зрения конечного пользователя.
Использование формальных моделей для анализа компонентов программно-конфигурируемых сетей
Использование формальных моделей для анализа компонентов программно-конфигурируемых сетей; формальные методы при анализе запросов, верификация композиций на наличие тупиков и зацикливаний, совместимость правил в коммутаторах; тестирование SDN контроллеров в контексте приложений и/или панели данных.

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

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

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

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

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