Introduction to Formal Methods of Software Engineering

2016/2017

Academic Year

RUS

Instruction in Russian

5

ECTS credits

Delivered at:

Department of Information Technologies in Business (Faculty of Computer Science, Economics, and Social Sciences)

Course type:

Elective course

When:

3 year, 1, 2 module

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

Аннотация

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

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

• получение высшего профессионально профилированного (на уровне бакалавра) образования, позволяющего выпускнику успешно работать в избранной сфере деятельности, обладать универсальными и предметно-специализированными компетенциями, способствующими его социальной мобильности и устойчивости на рынке труда, а именно: знакомство студентов с формальными методами программной инженерии, их практическим применением на различных этапах жизненного цикла программных систем
• развитие у студентов социально-личностных качеств: целеустремленности, организованности, трудолюбия, ответственности, самостоятельности, гражданственности, эмоционального интеллекта, приверженности этическим ценностям, коммуникативности, толерантности, повышение их общей культуры и мышления

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

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

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

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

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

• Текущая работа
• Аудиторная работа
• Экзамен

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

• Промежуточная аттестация (2 модуль)
  0.4 * Аудиторная работа + 0.2 * Текущая работа + 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