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

2024/2025

Учебный год

RUS

Обучение ведется на русском языке

6

Кредиты

Кто читает:

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

Статус:

Курс обязательный

Когда читается:

1-й курс, 1, 2 модуль

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

Камкин Александр Сергеевич

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

Аннотация

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

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

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

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

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

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

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

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

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

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

• 2024/2025 2nd module
  В рамках курса студентам предлагается выполнить одну контрольную работу (оценка — Окр) и два домашних задания (оценки — Одом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

Авторы

• Меликян Алиса Валерьевна
• Буцкая Евгения Александровна
• Камкин Александр Сергеевич