Формальная верификация

Therac-25 - медицинский ускоритель частиц. Программная ошибка в условиях гонки убила трёх пациентов. Ошибка существовала в коде годами, тесты её не находили. Формальная верификация нашла бы её за минуты.

• Amazon AWS верифицировал TLA+ 16 распределённых систем, нашёл 10 критических багов в спецификациях до реализации
• Intel после FDIV баг в Pentium ($475M убытков) внедрил model checking для FPU - Pentium 4 верифицирован формально
• NASA Deep Space 1 и Mars Pathfinder верифицированы SPIN перед запуском
• Microsoft верифицировал USB и файловую систему NTFS с помощью SLAM/SDV (Software Device Verifier)
• Airbus A380 fly-by-wire software верифицирован с Simulink Design Verifier и Polyspace

Model checking

Model checking - автоматическая верификация конечных систем: алгоритм обходит граф состояний и проверяет выполнимость спецификации на всех достижимых путях.

Основная проблема - взрыв пространства состояний: система из 100 булевых переменных имеет 2^100 состояний. BDD (Binary Decision Diagrams) и symbolic model checking позволяют работать с экспоненциальными пространствами компактно.

• Safety: "что-то плохое никогда не произойдёт" - инварианты
• Liveness: "что-то хорошее рано или поздно произойдёт" - прогресс
• Fairness: "процесс получит ресурс бесконечно часто" - планировщик
• SPIN: верификатор Promela-моделей, использован в NASA Mars Pathfinder
• CBMC: bounded model checker для C/C++, проверяет buffer overflows

TLA+ и спецификации

TLA+ (Temporal Logic of Actions) - язык спецификации Лесли Лэмпорта. Amazon использует TLA+ для верификации распределённых протоколов: DynamoDB, S3, EBS были проверены и найдены реальные баги.

TLA+ моделирует систему как последовательность состояний. Формулы описывают допустимые переходы (Next) и инварианты. TLC Model Checker проверяет все достижимые состояния модели.

• TLA+ применён в Amazon (16 систем, 10 найденных багов в спецификациях)
• Microsoft использует P (язык похожий на TLA+) для верификации USB стека
• Intel использовал model checking для верификации Pentium FPU после FDIV баг
• Azure Cosmos DB верифицирован с TLA+

SPIN и Promela

SPIN (Simple Promela INterpreter) - верификатор протоколов Жерара Хольцмана, разработан в Bell Labs. Использовался для верификации NASA Deep Space 1, Mars Pathfinder, протоколов 802.11.

SPIN использует on-the-fly model checking: LTL формула конвертируется в автомат Бюхи, его синхронный продукт с моделью проверяется на пустоту языка. Это избегает явного построения полного пространства состояний.

• Promela (Protocol Meta Language) - язык описания параллельных процессов
• LTL to Buchi: формула [] p автомат принимает все бесконечные слова где p всегда истинна
• Partial order reduction: сокращает пространство состояний, игнорируя независимые шаги
• Битовая хэш-компрессия: хранит посещённые состояния в bloom filter (false negatives возможны)

Темпоральная логика: LTL и CTL

Темпоральная логика расширяет классическую логику операторами времени. Два главных варианта: LTL (Linear Temporal Logic) рассуждает о путях, CTL (Computation Tree Logic) рассуждает о деревьях вычислений.

• LTL и CTL несравнимы: есть свойства, выразимые в одном, но не в другом
• AG EF reset (CTL) - нельзя выразить в LTL: квантификация по конкретному пути
• G (F p) (LTL) - нельзя выразить в CTL: путь где p истинна бесконечно часто
• CTL* включает оба: PSPACE-complete как LTL
• mu-calculus - наиболее выразительная темпоральная логика, включает CTL и LTL

Итоги

• Model checking - автоматический обход графа состояний, ограничен взрывом пространства
• TLA+ моделирует системы как последовательности состояний с темпоральными свойствами
• SPIN компилирует Promela + LTL в верификатор на C, on-the-fly алгоритм
• LTL рассуждает о линейных путях, CTL - о дереве вычислений, оба несравнимы

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

Формальная верификация пересекается с теорией автоматов, теорией сложности и математической логикой:

• Автоматы Бюхи — SPIN транслирует LTL в автоматы Бюхи для верификации бесконечных путей
• PSPACE-complete — Model checking LTL PSPACE-complete, CTL в P - отсюда разные инструменты
• Теория решётей — mu-calculus основан на теореме Тарского о фиксированных точках в решётках
• Typed lambda calculus — Coq и Lean реализуют Curry-Howard: типы = теоремы, программы = доказательства

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

• Почему формальная верификация не заменила тестирование в большинстве проектов?
• Что выгоднее верифицировать: спецификацию или реализацию? Каковы ограничения каждого подхода?
• Как partial order reduction помогает бороться со взрывом состояний в параллельных системах?

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

• ml-04
• ml-02