• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Магистратура 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) является результирующей
Список литературы

Список литературы

Рекомендуемая основная литература

  • Синицын С.В., Налютин Н.Ю. - Верификация программного обеспечения - Национальный Открытый Университет "ИНТУИТ" - 2016 - 445с. - ISBN: 978-5-94774-825-3 - Текст электронный // ЭБС ЛАНЬ - URL: https://e.lanbook.com/book/100665

Рекомендуемая дополнительная литература

  • Black, P. E., Ammann, P., & Ding, W. (2002). Model checkers in software testing [microform] / Paul E. Black, Paul Ammann, Wei Ding. Gaithersburg, MD : U.S. Dept. of Commerce, Technology Administration, National Institute of Standards and Technology, 2002. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsgpr&AN=edsgpr.000542901
  • Verger, A., & Pervanyuk, A. (2013). A Formalism to describe cyclogram testing models and perform model verification. Automation & Remote Control, 74(10), 1761–1770. https://doi.org/10.1134/S0005117913100159