Машинный перевод, не проверенный носителем языка. Эталоном служит английская версия.

Страницы видов сценариевПравить на GitHubИсточник: docs/kinds/by-kind/clock.md

clock (вид сценария)

Вид сценария движка v0.40.0, семейство Часы, синхронизация времени и holdover. Носит консультативный характер: результат анализа исследовательского и инженерного инструмента; это не навигационное оборудование с утверждённым типом и не служба обеспечения безопасности жизни. Каждая метка здесь принадлежит движку или матрице верификации; вид считается MODELLED, если матрица не указывает иное (как заслуживается метка: раздел Evidence в README).

Что делает#

Holdover часов относительно спецификации; необязательный ансамбль Монте-Карло (runs > 1).

Один прогон scenarios/clock-ensemble.toml сводится к следующему: scenario 91d2b6d10d14 | 200 runs | quantum holdover 6600s [6600-6600] p95 8.78e-4ns security n/a (no attack) | classical holdover 844s [220-2130] p95 167.0ns security n/a (no attack)

Входные параметры#

Из схемы (kshana kinds --json):

  • Обязательные поля: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Необязательные поля: runs, integrity

Пример scenarios/clock-ensemble.toml задаёт, среди прочего:

Поле Значение Единица
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s текст
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ текст
clock_classical.q_rw 0 1/s
clock_classical.q_wf 9.0000e-20 s^2/s
clock_classical.y0 5.0000e-10 1
clock_quantum.flicker_floor 1.0000e-16 1
clock_quantum.id optical-sr-lattice текст
clock_quantum.provenance Strontium optical lattice clock, space-oriented goal sigma_y текст
clock_quantum.q_rw 0 1/s
clock_quantum.q_wf 1.0000e-30 s^2/s
clock_quantum.y0 5.0000e-17 1

Запустите#

kshana scenarios/clock-ensemble.toml

Этот вид используют 6 поставляемых сценариев; остальные находятся в scenarios/.

Что он даёт#

Скалярные результаты этого прогона с единицами, которые указывает движок:

Результат Значение Единица
classical.availability.mean 0.295402 1
classical.availability.p05 0.115118 1
classical.availability.p50 0.242718 1
classical.availability.p95 0.680999 1
classical.filter_health.consistent true флаг
classical.filter_health.nees_chi2_lower_95 1.142439 1
classical.filter_health.nees_chi2_upper_95 3.092704 1
classical.filter_health.nees_mean 1.807227 1
classical.filter_health.nis_chi2_lower_95 0.912528 1
classical.filter_health.nis_chi2_upper_95 1.091418 1
График, который движок строит для scenarios/clock-ensemble.toml, вид clock

Доказательства#

MODELLED: строки матрицы верификации, называющие этот вид.

  • MODELLED Необязательный раздел [integrity] вида clock (clock_integrity::run): по заданным пресетам площадки и орбитальной группировки (geometry::sky_geometry), в каждую эпоху целостности, пока шкала времени GNSS не лишена сигнала, снимок RAIM (raim::snapshot_ Тесты: clock_integrity.rs.
  • MODELLED clock_log::read_input: один уровень разбора, который превращает файл часов RINEX (записи AS/AR одних именованных часов, версии 2 и от 3,00 до 3,04), ASCII-журнал фазы или частоты в стиле TimeLab либо журнал меток времени или интервалов TAPR TICC в единый pha Тесты: clock_log_allantools.rs.
  • MODELLED clock_log::read_input с форматами ptp4l, phc2sys, ts2phc, chrony-tracking и chrony-statistics: зафиксированное смещение строки сервопривода linuxptp (ns, собственная метка времени строки в квадратных скобках, показания до первого сообщения сервопривода о s2 исключены а
  • MODELLED Вид mission-thread: документ из фаз, каждая из которых относится к одному из восьми зарегистрированных видов; фазы выполняются по порядку, а ковариация 6x6, часы и система координат передаются по заданному правилу (carry; inflate, белый шум ускорения на заданном интервале Тесты: field_units_global.rs.
  • и ещё 1 в матрице.

Строки, которые задействовал сам прогон, с оракулом, который указывает им матрица (публичные источники названы там):

  • VALIDATED Девиация Аллана, модифицированная девиация Аллана и девиация Адамара + определение степенного шума с доверительными интервалами по χ². Oracle (ExternalDataset): NIST SP 1065 (Riley) / эталонные девиации Stable32 на NBS14
  • MODELLED Рост ошибки при выбеге в замкнутой форме + holdover до порога; классы квантовых часов. Oracle (ReferenceImpl): Многошаговая рекурсия ковариации clock_state (перекрёстная проверка внутри одной кодовой базы); лежащее в основе ядро дисперсии выбега и обращения holdover внешне проверено по scipy (см. «Clock-holdover coast-variance & threshold inversion»). Значения holdover по классам для красного шумового пола остаются MODELLED
  • MODELLED Часы с 3 состояниями (фаза/частота/дрейф) и фильтром Калмана по Ван Лоану, стабилизированным по Джозефу. Oracle (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), где F вычислена через scipy.linalg.expm, а Q — блочной матрицей Ван Лоана 1978 — независимая эталонная реализация, воспроизводящая всю траекторию полного фильтра kshana. Согласованность между реализациями: физика часов и калибровка по Аллану внешне не проверены, поэтому остаётся MODELLED. 0,30 внешнее сравнение, результат (остаётся MODELLED): по часам IGS final 30 s из 11 GPS Blo
  • MODELLED Объединённый посчётный показатель безопасности по эпохам: χ² с привлечением часов, RAIM, AGC, SQM. Oracle (ExternalDataset): параметры сценариев TEXBAT (Humphreys 2012) — характеристика, а не зафиксированные векторы. 0,30 внешнее сравнение, результат (остаётся MODELLED): на JammerTest 2024 (Bleik; данные под GPL-3.0) мониторы на уровне наблюдаемых (хи-квадрат с привлечением часов, RAIM, сбой решения) не подали тревоги в пределах 10 s ни при одном из 8 поддающихся оценке опубликованных начал спуфинга (где окно до начала было чистым, первая тревога приходила через 10,2–39 s после pu
  • MODELLED Детерминированные, хешируемые по сценарию, SBOM и кроссплатформенные эталонные проверки (golden). Оракул (ExternalDataset): соответствие SBOM официальной схеме JSON CycloneDX 1,5 (плюс допустимые идентификаторы SPDX) — внешний опубликованный стандарт, ноль ошибок валидации на всём графе зависимостей; часть о детерминизме FoM и побайтной воспроизводимости остаётся закреплённой проверкой внутренней согласованности, поэтому строка остаётся MODELLED

Ограничения#

Что отчёт самого прогона называет не смоделированным или не проверенным:

  • Holdover часов в условиях отсутствия GNSS — MODELLED, а не validated: он проверен по отдельной реализации в той же кодовой базе, независимой от проверяемого блока, но не являющейся внешним авторитетным источником. (матрица верификации (docs/MODELLED-RATIONALE.md))
  • Оценивание состояния бортовых часов — MODELLED, а не validated: оно проверено по отдельной реализации в той же кодовой базе, независимой от проверяемого блока, но не являющейся внешним авторитетным источником. (матрица верификации (docs/MODELLED-RATIONALE.md))
  • Обнаружение спуфинга — MODELLED, а не validated: одно из частных утверждений проверено внешне, но вся возможность составлена из смоделированных частей, поэтому остаётся Modelled. (матрица верификации (docs/MODELLED-RATIONALE.md))
  • Воспроизводимость и гарантии качества ПО — MODELLED, а не validated: одно из частных утверждений проверено извне, но вся возможность составлена из смоделированных частей, поэтому возможность остаётся Modelled. (матрица верификации (docs/MODELLED-RATIONALE.md))

См. также#