Высоконадёжные вычисления и системы реального времени
Содержание
Общие сведения
Предлагаемый курс адресован студентам в области инженерии программного обеспечения (ПО) и аппаратно-программных комплексов (системной инженерии), интересующихся проблемами построения систем реального времени (СРВ) с критическими требованиями по надежности.
К такого рода системам относятся, например, системы управления космической техникой, авиационной техникой (как пилотируемой, так и беспилотной), ядерными и химическими реакторами, высокоскоростным железнодорожным и беспилотным автомобильным транспортом, определенными медико-биологическими и финансовыми процессами, а также вооружениями и военной техникой. «Критический» уровень требований по надежности таких систем означает, что нарушение каких-либо свойств системы, составляющих надежность в широком смысле слова (например, функциональной или темпоральной корректности, отказоустойчивости, информационной безопасности и пр.) может привести к гибели людей или потенциально-неограниченному материальному ущербу.
За рубежом, главным образом во Франции и других европейских странах, уже в середине 1990-х годов инженерия высоконадежных СРВ оформилась в самостоятельный раздел информационных технологий в индустрии, а также в отдельную академическую дисциплину из области компьютерных наук. К сожалению, в Российской Федерации данное направление до сих пор недостаточно развито, и методы инженерии высоконадежных систем часто не применяются даже в тех областях, где их применение является уже общепринятой мировой практикой. Например, авария космического аппарата «Луна-25» в августе 2023 года произошла по причине непроведения темпорального анализа коммуникаций между задачами в бортовой системе управления, в результате чего не было своевременно обработано критическое сообщение от бортового акселерометра, что привело к столкновению аппарата с Луной.
Одним из факторов, до сих пор затрудняющих внедрение современных методов проектирования высоконадежных СРВ в российскую инженерную практику, является проблема подготовки соответствующих кадров. Данный курс призван восполнить этот пробел — он является первой и единственной в России образовательной программой, целью которой является подготовка отечественных специалистов в области высоконадежных СРВ.
Следует отметить, что высоконадежные СРВ одновременно являются, как правило, наукоемким программным обеспечением. Поэтому специалист в области высоконадежной системной инженерии должен владеть междисциплинарным комплексом знаний и навыков: — соответствующими знаниями из области компьютерных наук; — методами прикладной математики (дифференциальных уравнений, вариационного исчисления, теории управления); — а также иметь базовые знания в предметной области, связанной с управляемым объектом (например, в теоретической механике, аэродинамике или нейтронной физике).
Знания и навыки, приобретенные студентами в результате изучения данного курса, могут быть использованы в будущей профессиональной деятельности в структурах Роскосмоса, Росатома, Ростеха, РЖД и других высокотехнологичных российских компаний.
План занятий
- осенний семестр: 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 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 недели от момента выдачи задани
