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

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

Лучший по критерию «Полезность курса для расширения кругозора и разностороннего развития»

Лучший по критерию «Новизна полученных знаний»

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

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

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

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

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

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

Охват аудитории: для всех кампусов НИУ ВШЭ

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

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

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

Кредиты: 6

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

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

Аннотация

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

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

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

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

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

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

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

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

Лабораторная работа (ДЗ1)
Контрольная работа (КР1)
Экзамен (Экз)
Экзамен проводится в письменной форме с использованием синхронного прокторинга. Экзамен проводится на платформе 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 минут и более. При долговременном нарушении связи студент не может продолжить участие в экзамене. Процедура пересдачи аналогична процедуре сдач

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

2023/2024 учебный год 2 модуль
Оценка за первый семестр (итоговая оценка Оитог.1) складывается из накопленной оцен-ки 1 семестра (Онакопл.1) и оценки за устный экзамен в конце 2-го модуля (Оэкз.1): Онакопл.1 = Одом.зад.; Оитог.1 = 0.5⋅Онакопл.1 + 0.5⋅Оэкз.1.

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

Авторы

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

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