Формальные методы программной инженерии

Магистратура 2023/2024

Статус: Курс обязательный (Системная и программная инженерия)

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

Кто читает: Департамент программной инженерии

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

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

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

Охват аудитории: для своего кампуса

Преподаватели: Ломазова Ирина Александровна, Нестеров Роман Александрович

Прогр. обучения: Системная и программная инженерия

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

Кредиты: 9

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

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

Аннотация

В информатике и разработке программного обеспечения формальные методы представляют собой особый вид математически обоснованных методов для спецификации, разработки и верификации программных и аппаратных систем. Использование формальных методов для проектирования программного и аппаратного обеспечения мотивировано тем фактом, что, как и в других инженерных дисциплинах, выполнение соответствующего математического анализа может способствовать повышению надежности проекта. Формальные методы лучше всего описать как применение довольно широкого спектра теоретических основ информатики, в частности логических исчислений, формальных языков, теории автоматов и семантики программ, а также систем типов и алгебраических типов данных к задачам спецификации и верификации программного и аппаратного обеспечения. Формальные методы могут: (а) быть основой для описания сложных систем; (б) быть основой для рассуждений о системах; (в) обеспечивать поддержку разработки программ. В отличие от других подходов к проектированию систем, формальные методы используют математическое доказательство в качестве дополнения к системному тестированию для обеспечения правильного поведения. Поскольку системы усложняются, а безопасность становится все более важным вопросом, формальный подход к проектированию систем предлагает другой уровень страхования. Формальные методы отличаются от других методов проектирования использованием формальных схем проверки, правильность основных принципов системы должна быть доказана до того, как они будут приняты. Традиционный дизайн системы использует обширное тестирование для проверки поведения, но тестирование способно дать лишь конечные выводы. Э. Дейкстра и другие продемонстрировали, что тесты могут помочь обнаружить сбои и баги, но не могут гарантировать их отсутствие. Напротив, как только теорема доказана, она остается истинной. Очень важно отметить, что формальная проверка не устраняет необходимости в тестировании. Формальная проверка не может исправить неверные предположения в проекте, но она может помочь выявить ошибки в рассуждениях, которые в противном случае остались бы непроверенными. В нескольких случаях инженеры сообщали об обнаружении недостатков в системах после того, как они официально рассмотрели свои проекты.

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

изучение методов формальной спецификации и верификации поведения последовательных и параллельных систем с помощью различных подходов
изучение методов model checking для спецификации и верификации поведения распределенных информационных систем

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

владеть синтаксисом и семантикой формализмов для моделирования и анализа поведения распределенных систем
уметь моделировать различные классы распределенных систем
уметь формулировать и доказывать свойства дискретных систем с помощью алгебры процессов, сетей Петри и других подходящих формализмов

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

Формальные методы как основа надежности программного обеспечения
Дедуктивная верификация программ. Логика Хоара
Конечные автоматы
Сети Петри
Процессные алгебры
Бисимуляция
Concurrency Workbench: практика моделирования с помощью алгебры CCS
Model Checking: введение
Model Checking: свойства линейного времени, регулярные свойства
Model Checking: темпоральная логика линейного времени LTL
Model checking: практика верификации формул логики LTL
Model checking: логика ветвящегося времени CTL

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

O_accum1
Выполнение заданий на семинарах
O_exam1
O_accum2
O_htask2
O_exam2

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

2023/2024 учебный год 2 модуль
0.5 * O_accum1 + 0.5 * O_exam1
2023/2024 учебный год 4 модуль
0.12 * 2023/2024 учебный год 2 модуль + 0.3 * O_accum2 + 0.4 * O_exam2 + 0.18 * O_htask2

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