Высоконадёжные вычисления и системы реального времени

Общие сведения

Высоконадёжные вычисления и системы реального времени — понятия, связанные с обеспечением надёжности и своевременной реакции на внешние события. Эти термины обозначают разные области, и их реализация требует сочетания аппаратных и программных методов.

План занятий

• осенний семестр: 01 сентября – 14 декабря
• зачетная неделя: 15 – 21 декабря
• доп. выходные: 04 ноября 2025 г.

Руководитель курса и единственный преподаватель

Меркин Леонид Альбертович

Чат курса

чат в Telegram

Программа курса

В рамках программы изучаются следующие темы:

• Часть 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 недели от момента выдачи задани

Материалы занятий

Лекции