• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Магистратура 2020/2021

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

Статус: Курс обязательный (Системное программирование)
Направление: 09.04.04. Программная инженерия
Когда читается: 1-й курс, 1, 2 модуль
Формат изучения: без онлайн-курса
Прогр. обучения: Системное программирование
Язык: русский
Кредиты: 5
Контактные часы: 56

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

Аннотация

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

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

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

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

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

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

  • Введение
    Формальные методы в программной инженерии. История появления формальных методов и оценки эффективности их использования. Необходимость их использования.
  • Модели с конечным числом переходов, 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.
Список литературы

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

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

  • Автоматное программирование, Поликарпова, Н. И., 2009

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

  • 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