• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Статья
Detection of crawler traps: formalization and implementation—defeating protection on internet and on the TOR network

David B., Delong M., Filiol E. A.

Journal of Computer Virology and Hacking Techniques. 2021.

Глава в книге
Оптимизация компонентов многомодульных систем на основе решения автоматных уравнений.

Широкова Е., Евтушенко Л. Г., Лапутенко А. и др.

В кн.: 2020 Новые информационные технологии в исследовании сложных структур (ICAM 2020). Томск: Издательский Дом Томского государственного университета, 2020. С. 142-142.

Препринт
Preventive Model-based Verification and Repairing for SDN Requests

Burdonov I., Kossachev A., Nina Yevtushenko et al.

arxiv.org. Computer Science. Cornell University, 2020

Верификация программного обеспечения

2020/2021
Учебный год
RUS
Обучение ведется на русском языке
5
Кредиты

Преподаватель

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

Аннотация

Курс посвящен формальной верификации программ и моделей компьютерных систем. Цели — ознакомление студентов с базовыми принципами и методами формальной верификации и формирование у студентов навыков необходимых для практического использования рассмотренных методов. В основе лежат два класса методов: дедуктивная верификация и проверка моделей; рассматриваются методы формализации семантики программ (операционная и аксиоматическая семантика, структуры Крипке), методы формальной спецификации требований (программные контракты, темпоральная логика линейного времени), методы доказательства корректности программ (метод Флойда, теоретико-автоматный подход к проверке моделей в явной и символической формах). Для практики используются инструменты Frama-C/AstraVer/Why3 (дедуктивная верификация), а также Spin и NuSMV (проверка моделей).
Цель освоения дисциплины

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

  • Цель курса – изучение базовых принципов и методов верификации программного обеспече-ния (ПО); приобретение навыков, необходимых для практического применения методов верифика-ции ПО.
Планируемые результаты обучения

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

  • Знать базовые принципы формальной верификации ПО
  • Знать основные подходы к формальной верификации ПО
  • Понимать области применимости каждого из подходов
  • Понимать, что такое операционная семантика
  • Понимать, что такое аксиоматическая семантика
  • Понимать, что такое слабейшее предусловие программы
  • Знать определения частичной и полной программ
  • Знать методы Флойда (метод индуктивных утверждений и метод фундированных множеств)
  • 2. Понимать, что такое инвариант цикла (индуктивное утверждение)
  • Уметь находить инварианты циклов и оценочные функции
  • Уметь аналитически доказывать частичную и полную корректность программ
  • Владеть навыками спецификации программ в форме пред- и постусловий
  • Владеть навыками поиска инвариантов циклов
  • Знать основные возможности языка ACSL
  • Уметь пользоваться инструментами Frama-C/AstraVer
  • Понимать, что такое асинхронный параллелизм
  • Понимать, что такое синхронный параллелизм
  • Знать, что такое реагирующие системы
  • Знать алгоритм Петерсона взаимного исключения двух процессов
  • Знать логику LTL........
  • Знать, что такое структура Крипке
  • Уметь описывать свойства реагирующих систем в виде формул LTL
  • Знать, что такое автомат Бюхи и обобщенный автомат Бюхи
  • Знать метод проверки языка, описываемого автоматом Бюхи, на пустоту
  • Знать метод построения автомата Бюхи, распознающего пересечение языков, описываемых автоматами Бюхи
  • Знать алгоритм построения автомата Бюхи по формуле LTL
  • Уметь строить автомат Бюхи по формуле LTL
  • Знать схему теоретико-автоматного метода проверки моделей
  • Знать, что такое двоичные решающие диаграммы
  • Знать алгоритмы манипуляции с двоичными решающими диаграммами
  • Иметь представление о символических алгоритмах проверки моделей
  • Иметь представление об ограниченной проверке моделей
  • Владеть навыками спецификации свойcтв в виде формул LTL
  • Знать основные возможности языков Promela и SMV
  • Уметь пользоваться инструментами Spin и SMV
Содержание учебной дисциплины

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

  • Общие принципы формальной верификации
  • Формализация семантики языков программирования
  • Методы дедуктивной верификации программ
  • Инструментальные средства дедуктивной верификации программ
  • Параллельные программы и реагирующие системы
  • Темпоральная логика линейного времени
  • Теоретико-автоматный метод проверки моделей
  • Символический метод проверки моделей
  • Инструментальные средства проверки моделей
Элементы контроля

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

  • неблокирующий Экзамен (Э)
    Экзамен проводится дистанционно через Zoom. Технические требования: web-камера, микрофон, наушники / колонки, Zoom.
  • неблокирующий Домашняя работа 1 (ДР1)
  • неблокирующий Домашняя работа 2 (ДР2)
  • неблокирующий Контрольная работа (КР)
Промежуточная аттестация

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

  • Промежуточная аттестация (2 модуль)
    В рамках курса студентам предлагается выполнить одну контрольную работу (оценка — Окр) и два домашних задания (оценки — Одом1 и Одом2). Текущая оценка (Отек) рассчитывается как сред-нее арифметическое оценок Окр, Одом1 и Одом2: Отек = 1/3 *·(Окр + Одом1 + Одом2). Накопленная оценка рассчитывается следующим образом: Онакопл = 0,6 * Отек + 0,4 * Осам. В диплом выставляет результирующая оценка по учебной дисциплине, которая формируется по следующей формуле: Орезульт = 0,6 * Онакопл + 0,4 * Оэкзамен, где Оэкзамен — оценка за устный экзамен. Округление при вычислении результирующей оценки осуществляется в пользу студента.
Список литературы

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

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

  • Verification of Sequential and Concurrent Programs. (2009). Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsnar&AN=edsnar.oai.cwi.nl.14569

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

  • Baier, C., & Katoen, J.-P. (2008). Principles of Model Checking. Cambridge, Mass: The MIT Press. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=226091