Машинний переклад, не перевірений носієм мови. Еталоном є англійська версія.

Сторінки видів сценаріївРедагувати на GitHubДжерело: docs/kinds/by-kind/clock.md

clock (тип сценарію)

Тип сценарію рушія v0.40.0, родина Годинники, синхронізація часу та holdover. Лише консультативно: результат аналізу від дослідницького та інженерного інструмента; це не навігаційне обладнання із затвердженням типу і не послуга забезпечення безпеки життя. Кожна позначка тут належить рушієві або матриці верифікації; тип вважається MODELLED, якщо матриця не каже іншого (як заробляється позначка: розділ Evidence у README).

Що він робить#

Holdover годинника проти специфікації; необов'язковий ансамбль Монте-Карло (прогонів > 1).

Один прогін scenarios/clock-ensemble.toml підсумовується так: сценарій 91d2b6d10d14 | 200 прогонів | квантовий holdover 6600 с [6600-6600] p95 8.78e-4 нс безпека н/д (без атаки) | класичний holdover 844 с [220-2130] p95 167.0 нс безпека н/д (без атаки)

Входи#

Зі схеми (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 text
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ text
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 text
clock_quantum.provenance Стронцієвий оптичний решітчастий годинник, орієнтована на космос мета sigma_y text
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 flag
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 на єдиний фаз Тести: clock_log_allantools.rs.
  • MODELLED clock_log::read_input із форматами ptp4l, phc2sys, ts2phc, chrony-tracking і chrony-statistics: зафіксоване зміщення рядка серва linuxptp (нс, власна позначка часу рядка в дужках, показання до першого звіту серва s2 пропущено
  • MODELLED Тип mission-thread: документ із фаз, кожна з яких є одним із восьми зареєстрованих типів, що виконуються по черзі, а 6x6 коваріація, годинник і система відліку передаються далі за заданим правилом (carry; inflate, білий шум прискорення на заданому проміжку Тести: field_units_global.rs.
  • і ще 1 у матриці.

Рядки, які задіяв сам прогін, з оракулом, що його дає матриця кожному (публічні джерела названі там):

  • VALIDATED Девіація Аллана / модифікована / Адамара + ідентифікація степеневого шуму з довірчими інтервалами χ². Оракул (ExternalDataset): NIST SP 1065 (Riley) / еталонні девіації Stable32 на NBS14
  • MODELLED Замкнена форма зростання похибки за інерцією + holdover до порога; класи квантових годинників. Оракул (ReferenceImpl): Багатокрокова рекурсія коваріації clock_state (перехресна перевірка в тій самій кодовій базі); лежачі в основі ядро дисперсії інерційного руху та інверсії holdover зовнішньо перевірено проти scipy (див. «Clock-holdover coast-variance & threshold inversion»). Показники holdover для кожного класу з порогом червоного шуму лишаються MODELLED
  • MODELLED 3-становий (фаза/частота/дрейф) годинник Калмана van-Loan зі стабілізацією за Джозефом. Оракул (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), з F через scipy.linalg.expm та Q через блокову матрицю Van-Loan 1978 — незалежна еталонна реалізація, що відтворює повну траєкторію фільтра kshana. Узгодженість між реалізаціями: фізика годинника / калібрування Аллана не перевірені зовнішньо, тому це лишається MODELLED. 0,30 зовнішнє порівняння, знахідка (лишається MODELLED): на фінальних годинниках IGS 30 с для 11 блоків GPS
  • MODELLED Злитий покрокований FoM безпеки з χ² за допомогою годинника, RAIM, AGC, SQM на кожну епоху. Оракул (ExternalDataset): параметри сценаріїв TEXBAT (Humphreys 2012) — характеристика, а не закріплені вектори. 0,30 зовнішнє порівняння, знахідка (лишається MODELLED): на JammerTest 2024 (Bleik; дані GPL-3.0) монітори рівня спостережуваних величин (хі-квадрат за допомогою годинника, RAIM, збій розв'язку) не підняли тривоги протягом 10 с від жодного з 8 придатних до оцінки опублікованих початків спуфінгу (де вікно перед початком було чистим, перша тривога надходила через 10,2–39 с після
  • MODELLED Детерміновані, хешовані за сценарієм, SBOM + міжплатформні еталонні шлюзи. Оракул (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): одну частину твердження перевірено зовнішньо, але вся можливість складається із змодельованих частин, тож можливість лишається змодельованою. (матриця верифікації (docs/MODELLED-RATIONALE.md))
  • Відтворюваність і гарантування якості програмного забезпечення — MODELLED, а не перевірено за зовнішнім еталоном: підтвердження частини вимоги перевірено зовні, але вся можливість складається з обчислених за моделлю частин, тому можливість залишається обчисленою за моделлю. (матриця верифікації (docs/MODELLED-RATIONALE.md))

Див. також#