• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

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

2020/2021
Учебный год
RUS
Обучение ведется на русском языке
5
Кредиты
Статус:
Курс по выбору
Когда читается:
2-й курс, 4 модуль

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

Аннотация

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

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

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

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

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

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

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

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

  • неблокирующий Аудиторная работа
  • неблокирующий Самостоятельная работа
  • неблокирующий Экзамен
Промежуточная аттестация

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

  • Промежуточная аттестация (4 модуль)
    0.3 * Аудиторная работа + 0.3 * Самостоятельная работа + 0.4 * Экзамен
Список литературы

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

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

  • Малявко А. А. - ФОРМАЛЬНЫЕ ЯЗЫКИ И КОМПИЛЯТОРЫ. Учебное пособие для вузов - М.:Издательство Юрайт - 2019 - 429с. - ISBN: 978-5-534-04288-7 - Текст электронный // ЭБС ЮРАЙТ - URL: https://urait.ru/book/formalnye-yazyki-i-kompilyatory-438060
  • Математическая логика и теория алгоритмов: Учебник / Пруцков А.В., Волкова Л.Л. - М.:КУРС, НИЦ ИНФРА-М, 2016. - 152 с.: 60x90 1/16. - (Бакалавриат) (Переплёт 7БЦ) ISBN 978-5-906818-74-4 - Режим доступа: http://znanium.com/catalog/product/558694
  • Проектирование информационных систем : учебник и практикум для академич. бакалавриата, Грекул В.И., Коровкина Н.Л., 2017
  • Формальные языки и компиляторы/МалявкоА.А. - Новосиб.: НГТУ, 2014. - 431 с.: ISBN 978-5-7782-2318-9

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

  • Кудрявцев В. Б., Алешин С. В., Подколзин А. С. - ТЕОРИЯ АВТОМАТОВ 2-е изд., испр. и доп. Учебник для бакалавриата и магистратуры - М.:Издательство Юрайт - 2019 - 320с. - ISBN: 978-5-534-00117-4 - Текст электронный // ЭБС ЮРАЙТ - URL: https://urait.ru/book/teoriya-avtomatov-444091