Joint Department with the RAS Institute for System Programming

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

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

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

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

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

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

Введение
Формальные методы в программной инженерии. История появления формальных методов и оценки эффективности их использования. Необходимость их использования.
Модели с конечным числом переходов, 1
Конечные автоматы. Основные задачи анализа автоматов, их связь с анализом качества прикладного и системного программного обеспечения. Сложность задач анализа моделей с конечным числом переходов. Идентификация состояний в автоматных моделях. Построение проверяющих тестов с гарантированной полнотой на основе классических автоматных моделей.
Модели с конечным числом переходов, 2
Полнота проверяющих тестов. Многокомпонентные программные системы. Композиция автоматных моделей. Задачи анализа композиции; тестирование на совместимость, осцилляции и тупики. Автоматные модели с недетерминированным поведением, отношения конформности для недетерминированных автоматов и синтез тестов на соответствие спецификации относительно этих отношений. Тестирование в контексте. Пассивное тестирование.
Модели с конечным числом переходов, 3
Другие модели с конечным числом переходов: входо-выходные полуавтоматы, расширенные и временные автоматы, сети Петри. Обсуждение использования моделей с бесконечным числом состояний и переходов. Основные задачи анализа данных моделей, их связь с анализом качества прикладного и системного программного обеспечения. Построение проверяющих тестов с гарантированной полнотой на основе неклассических автоматных моделей.
Тестирование и верификация программного обеспечения на основе формальных моделей, 1
Методы тестирования программного обеспечения. Синтез проверяющих тестов для программных реализаций на основе расширенных и временных автоматов. Тестирование автоматных композиций на безопасность и совместимость, проверка наличия тупиков и зацикливаний в композициях неклассических автоматных моделей.
Тестирование и верификация программного обеспечения на основе формальных моделей, 2
Использование верификаторов (решателей) для верификации программного обеспечения. Синтез проверяющих тестов для программных реализаций на основе частичных автоматных моделей, возможно с ненаблюдаемым поведением.
Проектирование программного обеспечения с использованием формальных моделей и методов
Автоматное программирование. Автоматическое и полуавтоматическое проектирование программного обеспечения по автоматному описанию, например, UML. Достоинства и недостатки автоматической кодогенерации.

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

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

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

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

Contacts

Formal Methods in Software Engineering

Instructor

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

Аннотация

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

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

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

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

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

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

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

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