Магистратура
2020/2021![Цель освоения дисциплины](/f/src/global/i/edu/objectives.svg)
![Планируемые результаты обучения](/f/src/global/i/edu/results.svg)
![Содержание учебной дисциплины](/f/src/global/i/edu/sections.svg)
![Элементы контроля](/f/src/global/i/edu/controls.svg)
![Промежуточная аттестация](/f/src/global/i/edu/intermediate_certification.svg)
![Список литературы](/f/src/global/i/edu/library.svg)
Верификация программного обеспечения
Лучший по критерию «Новизна полученных знаний»
Статус:
Курс обязательный (Системное программирование)
Направление:
09.04.04. Программная инженерия
Где читается:
Факультет компьютерных наук
Когда читается:
1-й курс, 1, 2 модуль
Формат изучения:
без онлайн-курса
Преподаватели:
Камкин Александр Сергеевич
Прогр. обучения:
Системное программирование
Язык:
русский
Кредиты:
5
Контактные часы:
56
Программа дисциплины
Аннотация
Курс посвящен формальной верификации программ и моделей компьютерных систем. Цели — ознакомление студентов с базовыми принципами и методами формальной верификации и формирование у студентов навыков необходимых для практического использования рассмотренных методов. В основе лежат два класса методов: дедуктивная верификация и проверка моделей; рассматриваются методы формализации семантики программ (операционная и аксиоматическая семантика, структуры Крипке), методы формальной спецификации требований (программные контракты, темпоральная логика линейного времени), методы доказательства корректности программ (метод Флойда, теоретико-автоматный подход к проверке моделей в явной и символической формах). Для практики используются инструменты 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