Верификация программ

Бакалавриат 2020/2021

Статус: Курс по выбору (Программная инженерия)

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

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

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

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

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

Преподаватели: Петренко Александр Константинович

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

Кредиты: 5

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

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

Аннотация

Курс посвящен формальной верификации программ и моделей компьютерных систем. Цели — ознакомление студентов с базовыми принципами и методами формальной верификации и формирование у студентов навыков необходимых для практического использования рассмотренных методов. В основе лежат два класса методов: дедуктивная верификация и проверка моделей; рассматриваются методы формализации семантики программ (операционная и аксиоматическая семантика, структуры Крипке), методы формальной спецификации требований (программные контракты, темпоральная логика линейного времени), методы доказательства корректности программ (метод Флойда, теоретико-автоматный подход к проверке моделей в явной и символической формах). Для практики используются инструменты 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 модуль)
0.2 * Домашняя работа 1 (ДР1) + 0.2 * Домашняя работа 2 (ДР2) + 0.2 * Контрольная работа (КР) + 0.4 * Экзамен (Э)

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