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

2025/2026

Учебный год

RUS

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

6

Кредиты

Кто читает:

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

Статус:

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

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

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

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

Евтушенко Нина Владимировна

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

Аннотация

В рамках курса «Формальные методы в программной инженерии» изучаются основные принципы использования формальных методов в программной инженерии, в том числе, изучаются основные математические модели и методы их анализа и синтеза, формируются навыки анализа и проектирования программного обеспечения с использованием формальных методов. В результате освоения дисциплины студент должен знать основные математические модели и методы их анализа и синтеза для разработки и верификации/тестирования программного обеспечения; уметь применять известные формальные методы при проектировании программного обеспечения на языках высокого и низкого уровней; владеть навыками проектирования программного обеспечения в соответствии с его жизненным циклом, а также навыками верификации и тестирования программного обеспечения на основе формальных моделей.

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

• Изучение формальных методов в программной инженерии

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

• Владеть методами синтеза тестов с гарантированной полнотой на основе классических и неклассических автоматных моделей
• Владеть навыками проектирования программного обеспечения в соответствии с его жизненным циклом
• Знать основные формальные модели, использемые в программной инженерии

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

• Введение
• Модели с конечным числом переходов, 1
• Модели с конечным числом переходов, 2
• Модели с конечным числом переходов, 3
• Тестирование и верификация программного обеспечения на основе формальных моделей, 1
• Тестирование и верификация программного обеспечения на основе формальных моделей, 2
• Проектирование программного обеспечения с использованием формальных моделей и методов
• Формальные модели для анализа телекоммуникационных сервисов

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

• Лабораторная работа (ДЗ1)
• Лабораторная работа (ДЗ2)
  Уметь пользоваться верификаторами SPIN и TAMARIN для проверки безопасности телекоммуникационных протоколов
• Реферат
  Устное представление
• Экзамен (Экз)
  Экзамен проводится в письменной форме с использованием синхронного прокторинга. Экзамен проводится на платформе Moodle (https://moodle.org/?lang=ru) Прокторинг проводится на платформе Экзамус (https://hse.student.examus.net). К экзамену необходимо подключиться за 15 минут. На платформе Экзамус доступно тестирование системы. Компьютер студента должен удовлетворять следующим требованиям: https://elearning.hse.ru/data/2020/05/07/1544135594/Технические%20требования%20к%20ПК%20студента.pdf) Для участия в экзамене студент обязан: заранее зайти на платформу прокторинга, провести тест системы, включить камеру и микрофон, подтвердить личность. Во время экзамена студентам запрещено: общаться (в социальных сетях, с людьми в комнате), списывать. Кратковременным нарушением связи во время экзамена считается прерывание связи до 10 минут. Долговременным нарушением связи во время экзамена считается прерывание связи 10 минут и более. При долговременном нарушении связи студент не может продолжить участие в экзамене. Процедура пересдачи аналогична процедуре сдач

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

• 2025/2026 2nd module
  Итоговая оценка Оитог.1 складывается из накопленной оценки (Онакопл.1) и оценки за устный экзамен в конце 2-го модуля (Оэкз.1): Онакопл.1 = Одом.зад.=Реферат + ДЗ1 + ДЗ2; Оитог.1 = 0.5Онакопл.1 + 0.5Оэкз.1.

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

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

• Автоматное программирование, Поликарпова, Н. И., 2009
• Автоматное программирование. 2-е изд. - 978-5-4237-0075-1 - Поликарпова Н., Шалыто А. - 2020 - Санкт-Петербург: Питер - https://ibooks.ru/bookshelf/26248 - 26248 - iBOOKS
• Введение в теорию конечных автоматов, Гилл, А., 1966

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

• Aoki, T., & Taguchi, K. (2012). Formal Methods and Software Engineering : 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012: Proceedings. Berlin: Springer. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=566750
• Foster, E. C. (2014). Software Engineering : A Methodical Approach. [New York]: Apress. Retrieved from http://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=edsebk&AN=928129

Авторы

• Евтушенко Нина Владимировна
• Буцкая Евгения Александровна