Научно-исследовательский семинар "Системное программирование"

2019/2020

Учебный год

RUS

Обучение ведется на русском языке

3

Кредиты

Кто читает:

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

Статус:

Курс по выбору

Когда читается:

3-й курс, 1-3 модуль

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

Аннотация

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

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

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

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

• Способен решать проблемы в профессиональной деятельности на основе анализа и синтеза (УК-3)
• Способен оценивать потребность в ресурсах и планировать их использование при решении задач в профессиональной деятельности (УК-4)
• Способен использовать методы и инструментальные средства исследования объектов про-фессиональной деятельности (ПК-3)

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

• Предмет и методы системного программирования. Математические основы системного программирования
  Понятие системного слоя программного обеспечения. Особенности разработки и эксплуатации системного ПО. Виды системного ПО и виды инструментов разработки и анализа системного ПО. Теория множеств, исчисление предикатов, общая алгебра, теория графов, теория конечных автоматов, темпоральные логики, основы символьных вычислений, теории формальных языков, математическая лингвистика, теория вероятностей и математическая статистика, статистические методы анализа данных
• Инструменты поддержки жизненного цикла ПО. Управление требованиями. Формальные модели процессов разработки ПО
  Принципы системного проектирования комплексов программ. Cистемная и программная инженерия, процессы жизненного цикла сложных технических систем и программных комплексов. Декомпозиция требований, функций, процессов проектирования компонентов и комплексов программ. Повторное использование готовых компонентов при проектировании программных комплексов. Формальные модели процессов разработки программ (BPMN, BPEL, основы сетевого планирования).
• Методы проектирования программ на основе моделей.
  Виды моделей и парадигмы моделирования. Исполнимые (явные) модели, модели ограничений, алгебраические модели. Подходы к разработке и верификации программ на основе моделей (MDA, MDSE, MBT, SBT). Формальный аппарат моделирования программных систем: конечные автоматы (FSM), расширенные конечные автоматы (EFSM), системы размеченных переходов (LTS), сети Петри, темпоральные логики, алгебры сообщающихся процессов (CSP), исчисление сообщающихся машин (CCS). Формальные модели поддержки процессов про-ектирования (теория уточнений, методы уточнения в VDM, RAISE, Event-B). Языки проектирования программных и программно-аппаратных (UML, SysML, AADL).
• Методы верификации. Тестирование на формальных основе моделей
  Процессы верификации компонентов и комплексов программ. Трассирование требований к компонентам в комплексах программ. Организация процессов тестирования компонентов и комплексов программ. Методы динамической верификации. Процессы и методы тестирования программных модулей и компонентов. Функциональная декомпозиция системы тестирования на основе моделей. Примеры известных приложений подхода к тестированию на основе моделей. Логико-алгебраические и исполнимые модели. Абстрактные типы данных. Конечные автоматы. Расширенные конечные автоматы. Системы размеченных переходов. Использование разных видов моделей для описания функциональности. Теория соответствия (conformance) для FSM, LTS, EFSM. Управление абстракцией при спецификации и тестировании программных интерфейсов. Строгие методы определения соответствия между моделями разных уровней абстракции. Использование детерминированных и недетерминированных моделей при тестировании программных систем. Методы масштабирования тестовых сценариев при использовании многомашинных комплексов. Модели для генерации тестов микропроцессорной техники. Использование SMT-решателей для синтеза тестов (DART, Concolic testing, fazzing).
• Методы верификации. Дедуктивный анализ. Model checking, software model checking.
  Методы статической верификации. Понятие соответствия между моделью и реализацией, описание критериев соответствия, методы демонстрации и доказательства соответствия. Метод Флойда, методы верификации моделей. Известные инструменты для автоматизации процесса верификации (PVS, Isabelle/HOL, Frama-C, ACL2). Software model checking, метод предикатной абстракции, интерполяций Крейга, CEGAR, верификация моделей в ограничениях (BMC). Формальные модели памяти и их использование в дедуктивной верификации и в software model checking. Обобщенная постановка задачи соответствия моделей поведения программных систем. Случай исполнимых и неисполнимых спецификаций. Использование различных техник уточнения (refinement)
• Интеграция методов конструирования и верификации программных систем.
  Основные артефакты процессов конструирования и верификации программ. Цепочки инструментов, способы интеграции инструментов моделирования, проектирования и верификации программ.

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

• Самостоятельная работа
• Аудиторная работа
• Экзамен
  Экзамен проводится дистанционно через Zoom. Технические требования: web-камера, микрофон, наушники / колонки, Zoom.

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

• Промежуточная аттестация (3 модуль)
  0.25 * Аудиторная работа + 0.25 * Самостоятельная работа + 0.5 * Экзамен

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

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

• Кузнецов, А.С. Системное программирование : учеб. пособие / А.С. Кузнецов, И.А. Якимов, П.В. Пересунько. - Красноярск : Сиб. федер. ун-т 2018. - 170с. - ISBN 978-5-7638-3885-5. - Текст : электронный. - URL: https://new.znanium.com/catalog/product/1032183 - Текст : электронный. - URL: http://znanium.com/catalog/product/1032183

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

• Хэвиленд К., Грей Д., Салама Б. - Системное программирование в UNIX - Издательство "ДМК Пресс" - 2007 - 368с. - ISBN: 5-94074-008-1 - Текст электронный // ЭБС ЛАНЬ - URL: https://e.lanbook.com/book/1223