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

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

Предлагаемый курс адресован студентам в области инженерии программного обеспечения (ПО) и аппаратно-программных комплексов (системной инженерии), интересующихся проблемами построения систем реального времени (СРВ) с критическими требованиями по надежности.

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

За рубежом, главным образом во Франции и других европейских странах, уже в середине 1990-х годов инженерия высоконадежных СРВ оформилась в самостоятельный раздел информационных технологий в индустрии, а также в отдельную академическую дисциплину из области компьютерных наук. К сожалению, в Российской Федерации данное направление до сих пор недостаточно развито, и методы инженерии высоконадежных систем часто не применяются даже в тех областях, где их применение является уже общепринятой мировой практикой. Например, авария космического аппарата «Луна-25» в августе 2023 года произошла по причине непроведения темпорального анализа коммуникаций между задачами в бортовой системе управления, в результате чего не было своевременно обработано критическое сообщение от бортового акселерометра, что привело к столкновению аппарата с Луной.

Одним из факторов, до сих пор затрудняющих внедрение современных методов проектирования высоконадежных СРВ в российскую инженерную практику, является проблема подготовки соответствующих кадров. Данный курс призван восполнить этот пробел — он является первой и единственной в России образовательной программой, целью которой является подготовка отечественных специалистов в области высоконадежных СРВ.

Следует отметить, что высоконадежные СРВ одновременно являются, как правило, наукоемким программным обеспечением. Поэтому специалист в области высоконадежной системной инженерии должен владеть междисциплинарным комплексом знаний и навыков: — соответствующими знаниями из области компьютерных наук; — методами прикладной математики (дифференциальных уравнений, вариационного исчисления, теории управления); — а также иметь базовые знания в предметной области, связанной с управляемым объектом (например, в теоретической механике, аэродинамике или нейтронной физике).

Знания и навыки, приобретенные студентами в результате изучения данного курса, могут быть использованы в будущей профессиональной деятельности в структурах Роскосмоса, Росатома, Ростеха, РЖД и других высокотехнологичных российских компаний.

План занятий

• осенний семестр: 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 2022) для СРВ. Высоконадежный профиль 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 недели от момента выдачи задани

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

Лекции