Высоконадёжные вычисления и системы реального времени
Содержание
Общие сведения
Высоконадёжные вычисления и системы реального времени — понятия, связанные с обеспечением надёжности и своевременной реакции на внешние события. Эти термины обозначают разные области, и их реализация требует сочетания аппаратных и программных методов.
План занятий
- осенний семестр: 01 сентября – 14 декабря
- зачетная неделя: 15 – 21 декабря
- доп. выходные: 04 ноября 2025 г.
Руководитель курса и единственный преподаватель
Меркин Леонид Альбертович
Чат курса
Программа курса
В рамках программы изучаются следующие темы:
- Часть I: Основы теории систем реального времени (СРВ).
1. Критическое по надёжности ПО как специальный класс ПО. Его основные характеристики (в том числе real-time) и области применения -- аэрокосмическая, ядерная, химическая промышленность, высокоскоростной железнодорожный транспорт, национальная оборона.
2. Свойства надёжности ПО -- функциональные и нефункциональные (в первую очередь темпоральные). Опредедение СРВ, их основные свойства и примеры. Уровни критичности задач в СРВ (hard-, firm-, soft-real-time). Взаимосвязь между понятиями: СРВ, Concurrency, Parallelism.
3. Методы дизайна и верификации темпоральных свойств 1-процессорных СРВ. Алгоритмы планирования задач. Приоритеты задач и уравнение планируемости (schedulability equation). Периодические (time-driven) и спорадические (event-driven) задачи, их учет в уравнении планируемости.
4. Коммуникации между задачами, блокировки, проблема инверсии приоритетов, dеadlock и livelock. Алгоритм наследования приоритетов как решение данной проблемы. Модификация уравнения планируемости в условиях блокировок.
5. Распределенные СРВ (РСРВ). Шины и сети с детерминированным временем передачи данных (ARINC 664, AFDX). Проблема обеспечения темпоральной консистентности данных в РСРВ. Протокол time stamp'ов, учитывающих максимальное время доставки сообщений.
6. Холистический алгоритм планирования задач и коммуникаций в РСРВ, его итеративная реализация.
7. РСРВ в условиях возможных ошибок обработки и передачи данных. Алгоритмы поддержания консистентного состояния РСРВ. "Алгоритм византийских генералов". Связь с алгоритмами консистентности систем распределенного реестра.
- Часть II: Практические аспекты СРВ
8. Операционные системы (ОС, kernels, executives) и user-level компоненты СРВ. Требования к языкам программирования user-level компонент.
9. Стандарт Real-Time POSIX и операционные системы, его реализующие. Legacy стандарты API ОСРВ.
10. Linux как ОСРВ -- варианты, конфигурации, использование.
11. C и C++ как языки программирования СРВ. MISRA C / C++ guidelines. Concurrency в современных стандартах C++ (11--26) и её взаимосвязь с СРВ. Отсутствие собственно СРВ свойств в стандартах C++, и как решить эту проблему через underlying ОСРВ.
12. Язык программирования Ada (стандарт Ada 2012) для СРВ. Высоконадежный профиль Ada -- Ravenscar.
13. Задание для самостоятельного изучения основных элементов Ada, так как полностью изучить её за лекционное время невозможно).
14. ОСРВ RTEMS, её APIs (native, POSIX и исторические), применение в космической и зарубежной военной технике. Интеграция RTEMS с Ada. C++ bindings to RTEMS API.
15. ОСРВ FreeRTOS, её области применения. Ada и POSIX APIs.
16. Формально-верифицированное микроядро seL4. Применение в качестве hypervisor'a (для разделения компонент разного уровня критичности) и как РТОС. POSIX API (Ada binding пока отсутствует).
17. Практическое задание на основе RTEMS, FreeRTOS или seL4 (по выбору), Ada или C++.
- Часть 3: Методы инженерии высоконадежного наукоёмкого ПО
18. Взаимосвязь между "наукоёмким" ПО и критическими по надежности системам реального времени. Языки программирования наукоёмких приложений (Fortran не учитываем): функциональные (ML как основа всего!), Ada, C++.
19. Система типов языка программирования как отображение категорий реального мира на computer hardware. Система типов Hindley-Milner'а как основа "сильных" систем типов (и её варианты: Ada generics & C++ templates).
20. Необходимость отражения размерностей физических (в широком смысле) величин в системе типов. Dimension Types и их реализации в ML и C++. Библиотеки boost::units и DimTypes.
21. Необходимость отражения различных систем координат в системе типов для векторных вычислений. Библиотека SpaceBallistics (C++).
22. Проект с использованием библиотеки SpaceBallistics (в том числе интеграция с RTEMS): прототип системы управления космической ракетой-носителем.
23. От "сильных" систем типов к формальной верификации функциональных свойств ПО. Классы методов формальной верификации: для конечных автоматов (model checking), для логик 1-го порядка, логик высших порядков.
24. Организация процесса разработки высоконадежного ПО с использованием формальной верификации, от сбора требований до генерации (или написания) верифицированного программного кода.
25. Введение в B Method.
26. Введение в Spark Ada.
27. Очень краткое введение (если успеем) в Coq и Isabelle/HOL.
Проектные домашние задания
- (13) выше, срок 2 недели от моменты выдачи задания
- (17) выше, срок 3 недели от момента выдачи задания
- (22) выше, срок 3 недели от момента выдачи задани
