Joint Department with the RAS Institute for System Programming

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

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

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

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

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

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

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

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

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

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

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

Contacts

Software Verification

Instructor

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

Аннотация

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

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

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

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

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

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

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

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