Safety-Critical Systems

1996 год. Ракета Ariane 5, первый запуск Европейского космического агентства. На 37-й секунде полёта ракета теряет ориентацию и самоуничтожается. Стоимость потери: 370 млн долларов. Причина: 16-битный регистр в navigation software переполнился при попытке хранить 64-битное horizontal velocity. Код был унаследован от Ariane 4, где такие скорости физически не достигались. Не было ни единого unit теста на overflow - 'это же не нужно'. Сегодня та же ошибка не дошла бы до запуска: формальные методы и статический анализ ловят integer overflow на уровне компиляции. Safety-critical engineering - это и есть культура доказывать, что код не упадёт, даже когда никто не запускал тестов.

• **Boeing 737 MAX MCAS**: 2 крушения, 346 погибших, потеря 20 млрд долларов. Single point of failure (один датчик AoA), отсутствие redundancy, недокументированное поведение. Прямое нарушение DO-178C по SIL 4
• **Tesla FSD chip**: Dual NN на двух SoC, голосование, fall-back на rule-based safety monitor. ASIL D сертификация - первая в индустрии для ML-based ADAS
• **SpaceX Crew Dragon**: Triple-redundant flight computer + formal verification critical paths. После аварии на Boeing Starliner (2019) NASA настоял на этом подходе
• **Therac-25 (1985-1987)**: лучевой терапевт с race condition в коде - 3 пациента получили смертельные дозы радиации. Стартовая точка modern medical device safety regulation (IEC 62304)
• **Ariane 5 Flight 501 (1996)**: integer overflow в navigation software, 370 млн долларов уничтожены за 37 секунд. Все unit-тесты были на Ariane 4 параметрах - не масштабировали

IEC 61508 и уровни SIL

1980-е, Bhopal: утечка метилизоцианата на химзаводе Union Carbide убила 4000 человек за одну ночь. 1986-й, Therac-25: лучевой терапевт с race condition в коде выдал 100-кратные дозы радиации - погибли 3 пациента. После этих катастроф мир получил стандарт IEC 61508 (1998) и его дочерние стандарты: ISO 26262 для автомобилей, DO-178C для авионики, EN 50129 для железной дороги, IEC 62304 для медтехники. Все они формализуют одну вещь - **сколько может отказать система за единицу времени и какие методы должны это гарантировать**.

Стандарт не просто декларирует цифры - он перечисляет техники, которые должны применяться на каждом уровне. SIL 1: code review, unit tests, exception handling. SIL 2: добавляются static analysis, defensive programming. SIL 3: formal verification, semi-formal проверка алгоритмов, диверсификация компонентов. SIL 4: формальные методы (TLA+, Coq, SPARK Ada), полное доказательство корректности. Сертификация занимает 1-3 года и стоит $0.5-5M на проект - и это объясняет, почему обычный embedded SDK выглядит иначе, чем Boeing avionics SDK.

Парадокс stack: чем выше SIL, тем меньше функционала. SIL 4 фактически запрещает динамическую память, рекурсию, прерывания неизвестной вложенности, конструкции вроде указателей на функции. Java и C++ почти полностью под запретом. Используются подмножества: MISRA C, SPARK Ada, Frama-C. ML в safety-critical: Tesla на ASIL D обучает свои neural nets только на специально валидированных датасетах, и решения NN проверяются классическим safety-monitoring контуром (rule-based).

MISRA C: коробка с лезвиями

MISRA C - не язык, а guideline для написания на C, который не выстрелит в ногу. Возник в Motor Industry Software Reliability Association в 1998-м, сегодня - де-факто стандарт для автомобильного и авиа embedded. Около 150 правил, каждое - запрет конкретного источника багов: безусловные goto, рекурсия, динамическая память, implicit type conversion, side effects внутри условий. Идея: если из C убрать всё неоднозначное, останется подмножество, на котором статический анализатор может реально доказать отсутствие undefined behaviour.

Правила разделены на Required, Advisory, Mandatory. Deviation - формальный процесс: разработчик пишет обоснование, safety officer подписывает, документ хранится 30 лет (срок жизни airbus). Каждое нарушение, не оформленное deviation, блокирует certification. Toyota после случая unintended acceleration в 2009 году получила штраф $1.2B - расследование NASA нашло 7000 нарушений MISRA в их коде throttle controller. С тех пор отрасль не шутит с этим.

Аналог MISRA в Rust - subset SPARK для Rust (на стадии исследования) и unsafe-free подмножество для embedded. В C++ есть AUTOSAR C++14 (300+ правил поверх MISRA C++). Современные подмножества движутся к ownership-based безопасности: Rust ASIL-B готовится к certification, и через 5-10 лет ожидается ASIL D-готовый Rust. Прорыв сравним с переходом от ассемблера к C в 1980-х.

Статический анализ: доказать без запуска

Юнит-тесты доказывают наличие багов, формальный анализ - их отсутствие (Дейкстра, 1972). Идея: построить математическую модель программы и доказать утверждения о всех возможных её исполнениях, не запуская ни одного. Технологии разные: abstract interpretation (Polyspace, Astrée) ищет numerical overflow, division by zero, array bounds. Model checking (CBMC) перебирает все возможные состояния автомата на ограниченной глубине. Deductive verification (SPARK, Frama-C/WP) требует от разработчика писать annotations и автоматически проверяет их через SMT-solvers (Z3, Alt-Ergo).

Airbus A380 использует SPARK Ada для всей fly-by-wire системы. 200 000 строк кода, формально верифицированные через AdaCore Verification Studio. Найдено 0 багов в production за 15 лет эксплуатации. Сравните с типичным embedded C проектом: 1-10 багов на 1000 строк кода после shipping. Прецедент: NASA Mars Curiosity rover - SPARK для critical sequencing. Аналогия в ML: формальная верификация устойчивости neural nets к adversarial examples (DeepPoly, ERAN) - тот же tooling, новый домен.

Стоимость доказательства - в человеко-годах. SPARK Ada разработка дороже стандартного C в 3-5 раз, но bug rate ниже в 100-1000 раз. Для авионики, где один баг стоит самолёта (Boeing 737 MAX MCAS - 346 погибших, потеря $20B), это окупается мгновенно. Для домашнего ESP32-проекта - bezsmysslennaya overkill. Критерий выбора: цена одного отказа vs цена доказательства.

Резервирование: одной системы недостаточно

Каким бы тщательным ни был код, hardware ломается. Cosmic rays переключают биты в RAM (один single-event upset на гигабайт памяти в день на уровне моря, чаще в полёте). Конденсаторы стареют. MOSFET-ы получают electromigration через 10 лет. На SIL 3-4 одного процессора недостаточно физически. Применяются три уровня резервирования: **dual-channel** (два одинаковых канала с голосованием), **triple modular redundancy** (TMR - три канала, голосование по большинству), **diversity** (два канала с разной реализацией - один на C, другой на Ada, разные процессоры, разные команды разработки).

Boeing 777 имеет 3 Primary Flight Computers разных вендоров (AMD 29050, Intel 80486, Motorola 68040), три разных компилятора, три независимые команды разработки одних и тех же спецификаций. Это **diversity-style TMR** - защита от systematic faults, не только random. Если в спецификации Boeing была ошибка, она присутствует во всех трёх, но если ошибся один программист на C - двое других, писавшие на Ada и Pascal, отдадут правильный ответ. Стоимость? Тройной бюджет разработки. Цена ошибки? 350 жизней.

Tesla Autopilot ASIL D реализует похожий принцип через два независимых SoC FSD (FSD-1 и FSD-2), каждый со своей нейросетью на разных кадрах. Если их выводы разойдутся слишком сильно - downgrade до limp mode, передача управления водителю. SpaceX Dragon: 3 flight computers с byzantine fault tolerance в bare-metal C, формально верифицированы. Когда один процессор посчитает, что нужно гасить двигатели на 50%, а другие два - на 100%, голосование выдаёт 100%, и первый помечается failed.

Связанные темы

Safety-critical engineering стоит на пересечении hardware reliability, formal methods и process culture:

• RTOS и детерминированные планировщики — Base для предсказуемого WCET и safety scheduling
• Operational semantics — Формальная семантика языка - prerequisite для доказательной верификации
• AI Guardrails — Те же принципы в applied AI: monitor LLM outputs через rule-based safety net
• Low-power режимы — Watchdog и safe-state recovery опираются на правильный sleep management

Ключевые идеи

• **IEC 61508 и SIL** задают вероятность отказа в час: SIL 1 (10^-5) для термостатов, SIL 4 (10^-9) для авионики. Каждый уровень требует своего набора техник
• **MISRA C** - подмножество C, на котором статический анализатор может доказывать absence of UB. Запрет malloc, recursion, function pointers - всего, что мешает детерминизму
• **Статический анализ** (Frama-C, SPARK, Polyspace, Astree) доказывает отсутствие багов на всех возможных входах, без запуска. Дороже разработки в 3-5x, bug rate ниже в 100-1000x
• **Резервирование** - физический закон safety-critical: TMR с голосованием для random failures, diversity (разные процессоры, языки, команды) для common-mode failures
• **Watchdog + safe state** - последний рубеж: если всё остальное упало, hardware timer форсит reset и переход в безопасное состояние

Вопросы для размышления

• Если NN классифицирует препятствие на дороге с уверенностью 99.99% - этого хватает для ASIL D? Какие проверки нужно добавить, чтобы интегрировать ML в safety-critical стек?
• Почему Boeing использует три разных архитектуры процессоров (AMD, Intel, Motorola) с тремя разными командами? Что произошло бы при TMR на трёх одинаковых системах с одинаковым кодом?
• Где грань между разумной safety и paranoid overkill? Когда формальная верификация стоит 5x бюджета, а когда code review достаточно?

Связанные уроки

• emb-13 — Low-power режимы важны для long-running safety систем (watchdog)
• emb-12 — RTOS даёт детерминированный планировщик - база для safety
• rts-08 — Worst-case execution time анализ обязателен для SIL 3/4
• plt-14-operational-semantics — Формальная семантика - база для верификации safety кода
• aie-33-guardrails — Guardrails для LLM - тот же подход через резервирование и проверки
• dl-09 — Safety ML моделей в Tesla Autopilot - продолжение IEC 61508 в эпоху нейросетей
• rts-01