Системы реального времени
Formal Methods для RT
Pentium FDIV bug, 1994: математик вычислял простые числа и получил неправильный результат от CPU. Intel потратила 475 млн долларов на замену процессоров. После этого Intel применила formal verification. Вопрос: можно ли доказать корректность программы математически, а не тестами?
- **Amazon AWS:** TLA+ используется для верификации протоколов DynamoDB, S3, EBS. В 2014 году Amazon обнаружил 10 критических багов, включая потенциальную потерю данных, недостижимых обычным тестированием.
- **Airbus:** UPPAAL применяется для верификации части flight management software. Timed Automata позволяют доказать соответствие timing requirements без исчерпывающего тестирования всех сценариев.
- **seL4 microkernel:** Первая и единственная ОС с полным математическим доказательством корректности реализации. Используется в военных БПЛА Boeing. 200000 строк Isabelle proof на 8700 строк C.
Model Checking: перебор пространства состояний
В 1994 году Intel выпустила процессор Pentium с ошибкой в блоке деления с плавающей точкой. Баг обнаружил математик, вычисляя простые числа - он получил неправильный результат. Потери Intel: 475 млн долларов и репутация. После этого Intel применила formal verification для последующих CPU. Model checking - это метод, при котором система представляется в виде конечного автомата, а свойства задаются формулами темпоральной логики. Алгоритм автоматически проверяет все достижимые состояния системы - не запускает тесты, а математически перебирает граф переходов.
Темпоральная логика CTL (Computation Tree Logic) позволяет выразить свойства типа: AG(request -> AF response) - «всегда: если запрос, то рано или поздно придёт ответ». LTL (Linear Temporal Logic) работает с путями: G(p -> F q). Для real-time систем критично TCTL - Timed CTL, где формула может содержать временные ограничения: AF<=10ms(response). Model checker находит контрпример, если свойство нарушается.
Что делает model checker при обнаружении нарушения проверяемого свойства?
Timed Automata: время как первый класс
Обычные конечные автоматы не знают, сколько времени прошло между переходами. Для real-time систем это катастрофа: нельзя выразить «watchdog должен сработать через 10 мс», «задача должна ответить за 5 мс». Timed Automata, предложенные Алуром и Диллом в 1994 году, решают эту проблему добавлением часов (clocks) - непрерывно растущих переменных. Переходы могут проверять значения часов (guard: x < 10) и сбрасывать их (reset: x := 0). Состояния могут иметь invariant: x <= 10, который запрещает системе оставаться в состоянии дольше нормы.
Timed Automata верифицируемы: несмотря на непрерывное время, пространство состояний можно конечно разбить на regions - классы эквивалентности по поведению. Два момента времени эквивалентны, если они не различимы с точки зрения поведения автомата. Количество regions экспоненциально от числа часов и числовых констант в guards. На практике инструменты используют более эффективные zones (DBM - Difference Bound Matrices).
Зачем в Timed Automata нужны invariants у состояний в дополнение к guards на переходах?
UPPAAL: практический инструмент верификации
UPPAAL - совместная разработка Uppsala University и Aalborg University, один из наиболее используемых инструментов для верификации real-time систем. Он реализует расширение Timed Automata: несколько автоматов работают параллельно, синхронизируясь через каналы (!/?). Вся система - это сеть автоматов. Swarm of satellites, протокол ABS, медицинские устройства, авионика - всё это верифицировалось в UPPAAL. Airbus использует UPPAAL для верификации части flight management software.
UPPAAL поддерживает три режима: Simulator (пошаговое выполнение), Verifier (model checking с CTL формулами), Tracer (воспроизведение counterexample). Язык запросов: A[] - для всех путей всегда, E<> - существует путь где когда-нибудь, A<> - для всех путей когда-нибудь, E[] - существует путь где всегда. Плюс TCTL расширения: A[] (Clock <= deadline).
Что означает запрос A[] not deadlock в UPPAAL?
Верификация на практике: применение в индустрии
Формальные методы долго считались уделом академиков. Amazon AWS переломила этот стереотип: в 2014 году компания опубликовала статью о применении TLA+ для верификации распределённых протоколов (DynamoDB, S3, EBS). Инженеры нашли 10 критических багов, включая потенциальную потерю данных при конкретной последовательности сбоев. Без формальной спецификации эти сценарии прошли бы через все тесты. Для real-time систем формальная верификация - не академика, а инструмент, который заменяет тысячи часов тестирования.
Практические ограничения: state space explosion ограничивает применимость model checking для больших систем. Решения: abstraction (убрать несущественные детали), compositional verification (верифицировать компоненты по отдельности), bounded model checking (проверять ограниченную глубину). Для DO-178C DAL-A формальные методы признаются в качестве альтернативного метода верификации, снимающего часть требований по тестовому покрытию.
Формальные методы - это только для академических задач, в реальных проектах они слишком медленные и дорогие
Amazon, Airbus, Microsoft применяют формальные методы в production. TLA+ нашёл баги в S3 и EBS, UPPAAL используется в авиационных системах
Стоимость формальной верификации выше, чем обычного тестирования. Но стоимость необнаруженного бага в safety-critical системе несравнимо выше. Amazon подсчитал, что TLA+ окупается уже на первом найденном баге потенциальной потери данных.
Почему seL4 microkernel считается выдающимся достижением в области верификации ПО?
Ключевые идеи
- **Model checking** - автоматический перебор всех состояний системы и проверка CTL/LTL формул. При нарушении выдаёт контрпример - конкретный путь выполнения.
- **Timed Automata** расширяют автоматы часами (clocks) и invariants, позволяя выражать и верифицировать timing requirements. UPPAAL реализует этот формализм для параллельных систем.
- **Формальные методы в индустрии** применяет Amazon (TLA+), Airbus (UPPAAL), Microsoft (P language). DO-178C признаёт их как альтернативу части тестовых требований для DAL-A.
Связанные темы
Формальные методы пересекаются с требованиями стандартов безопасности и практикой планирования задач:
- Стандарты безопасности DO-178C, ISO 26262 — DO-178C DAL-A признаёт формальную верификацию как альтернативный метод, снижающий требования к тестовому покрытию
- Планировщики и WCET — WCET analysis - это частный случай формальной верификации: доказательство верхней границы времени выполнения задачи
Вопросы для размышления
- Model checking страдает от state space explosion. Как compositional verification решает эту проблему, и какие допущения необходимо сделать для её применения?
- TLA+ позволил Amazon найти баги в S3 и EBS, которые не нашло тестирование. Какой класс ошибок наиболее сложно обнаружить тестами, но легко - model checking?
- seL4 имеет 200000 строк proof на 8700 строк кода. Что происходит с доказательством при изменении одной строки реализации, и как это влияет на maintainability?