Кратко — предложенная методика состоит из многоуровневой формальной спецификации + верификации на моделях и коде, покрывающей как детерминированную логику, так и непрерывную/стохастическую динамику, плюс сценарное тестирование в симуляции и доказательства/статистические гарантии для полевых запусков. Ниже — конкретная структура, модели, методы и требования к сертификационным артефактам.
1) Формальная спецификация требований
- Разделение на уровни: системные требования → компонентные контракты (assume‑guarantee) → интерфейсные предположения о окружении.
- Используемые логики:
- Логика LTL/CTL для дискретных свойств: пример $\square (\text{obstacle}\to ◊\text{brake})$.
- Сигнальная/метрическая временная логика для реальных сигналов: STL/MTL, пример: $\square (d(t)>d_{\min })$, или «если A, то B в течение 2 с»: $\square (A\to {◊}_{[0,2]}B)$.
- Гибридные спецификации для смешанных непрерывно-дискретных свойств.
- Формализация контроллеров как гибридных автоматов: используем представление $(Q,X,f,Init,Inv,E,G,R)$ где $Q$ — дискретные режимы, $X$ — непрерывные переменные и т.д.
2) Формальные модели системы
- Дискретное управление: детерминированные/недетерминированные конечные автоматы (FSM), timed automata (UPPAAL).
- Динамика движения и сенсоров: гибридные автоматы / модели непрерывной динамики (SpaceEx, HyST).
- Поведение участников движения: POMDP/стохастические модели для непредсказуемых агентов.
- Контракты компонентов (assume-guarantee), чтобы локально верифицировать и затем композиционно доказывать свойства системы.
3) Формальные методы верификации
- Model checking:
- UPPAAL/Spin для дискретно-временных свойств; статистическое model checking для стохастики.
- Reachability анализ для непрерывной части (Flow*, SpaceEx, CORA).
- Теоремы и доказательства:
- KeYmaera X для гибридных систем; Isabelle/HOL или Coq для критически важной логики/контрактов.
- SMT/Static analysis:
- Z3, CBMC, Frama‑C/ASTree для проверки реализации, инвариантов и отсутствия переполнений.
- Верификация моделей ML-компонентов:
- Формальная верификация свойств (Reluplex/ERAN) + верификация устойчивости к небольшим искажениям; если невозможна — статистические гарантии (см. ниже).
4) Тестовое покрытие и критерии
- Кодовое покрытие: statement, branch, и обязательное MC/DC для критических модулей (уровень ASIL D).
- Спецификационное покрытие: каждая требование ↔ набор тестов (requirements-based coverage).
- Модельное покрытие: состояние/переход/режим coverage в FSM; покрытие зон в непрерывном пространстве (разбиение параметрического пространства).
- Сценарное/семантическое покрытие:
- Набор параметрических сценариев с покрытием краевых условий, комбинаций (pairwise, $n$-wise), распределений интенсивности.
- Метрики «coverage of operational design domain (ODD)»: покрытие погоды, освещённости, скоростей, плотности трафика.
- Для редких событий — гарантии через статистическую проверку: для уровня доверия $1-\alpha$ и допускной ошибке $ϵ$ количество независимых запусков $N$ можно оценивать, например, через Chernoff: $$N\ge \frac{\ln (1/\alpha )}{2{ϵ}^2}.$$
5) Симуляции сцен и их генерация
- Уровни тестирования: MIL → SIL → HIL → VIL → реальный тест.
- Инструменты: CARLA, LGSVL, Prescan/IPG, VeHIL для HIL.
- Сценарии:
- Базовые сценарии (NHTSA/PEGASUS/ASAM OpenSCENARIO форматы).
- Стресс-тесты: adversarial/scenario fuzzing (search‑based testing, genetic algorithms, coverage‑guided RL).
- Falsification (S-Taliro, Breach) для поиска контрпримеров против STL/LTL спецификаций.
- Importance sampling / rare-event simulation для оценки рисков очень редких аварийных событий.
- Верификация замкнутой петли: симулируем сенсоры, планирование, контроль и динамику окружения вместе; фиксируем метрики времени реакции, минимальной дистанции, безопасных состояний.
6) Runtime assurance и защита в реальном времени
- Синтез мониторинга из формальных спецификаций (STL → онлайн‑монитор), генерация аварийных флагов.
- Архитектура Simplex / verified fallback controller: основной сложный контроллер + простой проверенный «safety supervisor».
- Контроль барьерами (CBF) и online reachability для гарантии безопасных действий.
- Логирование и онлайн‑валидирование предположений об окружении (assumption monitoring).
7) Сертификация и артефакты (соответствие стандартам)
- Следовать ISO 26262 (ASIL), ISO/PAS 21448 (SOTIF), ISO 21434 (cybersecurity), UNECE WP.29 и (по необходимости) DO‑178C для ПО.
- Обязательные артефакты:
- Формальные требования, контракты, модель системы и трассируемость требований → код → тесты.
- Отчёты model checking / theorem proving с контрпримерными трассами и их разрешением.
- Покрытие: MC/DC отчёты, модельное и сценарное покрытие с порогами, принятыми в проекте.
- Результаты HIL/real tests и статистические оценки риска для полевых запусков.
- Safety case (например GSN) объединяющий доказательства, тесты, риски и планы mitigations.
- SOTIF‑ориентированные шаги: идентификация функциональных ограничений, сценарное тестирование на «небезопасное поведение при отсутствии отказа», доказательства уменьшения риска.
8) Практический workflow (коротко)
- Формализовать требования (STL/LTL), разделить по контрактам.
- Создать модели: discrete FSM + hybrid dynamics + stochastic agents.
- Произвести model checking + reachability + theorem proving по ключевым свойствам.
- Параллельно генеративно тестировать в симуляции (falsification, search‑based, rare‑event).
- Верифицировать код (SMT, static analysis), требуемое покрытие (MC/DC).
- HIL/vehicle testing с мониторингом и сбором данных; обновлять модели и тесты.
- Подготовить safety case и доказательства для сертификации по ISO/UNECE.
9) Рекомендации по инструментам (примерно)
- Model checking / timed automata: UPPAAL, Spin.
- Hybrid reachability: SpaceEx, Flow*, Hylaa.
- Theorem proving: KeYmaera X (гибриды), Isabelle, Coq.
- Falsification/monitoring: Breach, S‑Taliro, RTAMT.
- Simulation & scenarios: CARLA, LGSVL, ASAM OpenSCENARIO/OpenDRIVE форматы.
- Code verification: Frama‑C, CBMC, Z3.
Заключение: сочетание формальных спецификаций (STL/LTL, гибридные автоматы), строгой верификации (model checking, reachability, theorem proving), статистической оценки для ML/стохастики, всеуровневого сценарного тестирования с покрытием и runtime monitoring + подготовка safety case под ISO 26262/SOTIF даёт практически реализуемую методику минимизации риска критических ошибок.