clock (druh scénáře)

Druh scénáře enginu v0.40.0, rodina Hodiny, časování a holdover. Pouze poradní charakter: výstup analýzy z výzkumného a inženýrského nástroje; nejde o typově schválené navigační zařízení ani o službu z oblasti bezpečnosti života. Každé označení zde pochází z enginu nebo z verifikační matice; druh je MODELLED, pokud matice neuvádí jinak (jak se označení získává: oddíl Evidence v README).

Co dělá#

Holdover hodin oproti specifikaci; volitelný soubor Monte Carlo (runs > 1).

Jeden běh scenarios/clock-ensemble.toml se shrnuje takto: scénář 91d2b6d10d14 | 200 běhů | kvantový holdover 6600s [6600-6600] p95 8.78e-4ns zabezpečení n/a (žádný útok) | klasický holdover 844s [220-2130] p95 167.0ns zabezpečení n/a (žádný útok)

Vstupy#

Ze schématu (kshana kinds --json):

• Povinná pole: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
• Volitelná pole: runs, integrity

Příklad scenarios/clock-ensemble.toml mimo jiné nastavuje:

Spusťte jej#

kshana scenarios/clock-ensemble.toml

6 přibalených scénářů používá tento druh; ostatní jsou v scenarios/.

Co poskytuje#

Skalární výsledky tohoto běhu s jednotkami, které engine uvádí:

Důkazy#

MODELLED: řádky verifikační matice, které tento druh jmenují.

• MODELLED Volitelný oddíl [integrity] druhu clock (clock_integrity::run): z uvedeného stanoviště a předvoleb konstelace (geometry::sky_geometry) v každé epoše integrity, dokud časová osa GNSS není odepřena, snapshot RAIM (raim::snapshot_ Testy: clock_integrity.rs.
• MODELLED clock_log::read_input: jedna vrstva parseru, která převádí soubor hodin RINEX (záznamy AS/AR jedněch pojmenovaných hodin, verze 2 a 3,00 až 3,04), ASCII záznam fáze nebo frekvence ve stylu TimeLab nebo záznam časových značek či intervalů TAPR TICC na jednotnou pha Testy: clock_log_allantools.rs.
• MODELLED clock_log::read_input s formáty ptp4l, phc2sys, ts2phc, chrony-tracking a chrony-statistics: zaznamenaný offset řádku servo linuxptp (ns, vlastní závorková časová značka řádku, odečty před prvním hlášením s2 servem vynechány a
• MODELLED Druh mission-thread: dokument fází, z nichž každá je jedním z osmi registrovaných druhů, spouštěných postupně, přičemž kovariance 6x6, hodiny a soustava se předávají podle stanoveného pravidla (carry; inflate, šum bílého zrychlení po stanovenou mezeru Testy: field_units_global.rs.
• a 1 další v matici.

Řádky, které běh sám procvičil, s orákulem, které matice každému dává (veřejné zdroje jsou tam uvedeny):

• VALIDATED Allanova / modifikovaná / Hadamardova odchylka + identifikace šumu s mocninným zákonem s intervaly spolehlivosti χ². Oracle (ExternalDataset): NIST SP 1065 (Riley) / referenční odchylky Stable32 na NBS14
• MODELLED Růst chyby při dobíhání v uzavřeném tvaru + holdover do prahu; třídy kvantových hodin. Oracle (ReferenceImpl): Vícekroková rekurze kovariance clock_state (křížová kontrola ve stejné kódové základně); podkladové jádro rozptylu dobíhání a inverze holdoveru do prahu je externě ověřeno proti scipy (viz 'Clock-holdover coast-variance & threshold inversion'). Hodnoty holdoveru podle třídy při úrovni červeného šumu zůstávají MODELLED
• MODELLED 3stavové (fáze / frekvence / drift) Kalmanovy hodiny van Loan, Joseph-stabilizované. Oracle (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), s F přes scipy.linalg.expm a Q přes blokovou matici Van Loan 1978 -- nezávislá referenční implementace reprodukující celou trajektorii filtru Kshany. Konzistence mezi implementacemi: fyzika hodin a kalibrace Allanovy odchylky nejsou ověřeny proti nezávislé vnější referenci, proto zůstává MODELLED. 0,30 vnější srovnání, zjištění (zůstává MODELLED): na hodinách IGS final 30 s z 11 GPS Blo
• MODELLED Hodinami podpořené χ², RAIM, AGC, SQM slučované do bezpečnostního FoM pro každou epochu. Oracle (ExternalDataset): parametry scénářů TEXBAT (Humphreys 2012) -- charakterizace, nikoli připnuté vektory. 0,30 vnější srovnání, zjištění (zůstává MODELLED): na JammerTest 2024 (Bleik; data GPL-3.0) monitory na úrovni pozorování (chí-kvadrát podpořený hodinami, RAIM, selhání řešení) nevyvolaly žádný alarm do 10 s od žádného z 8 vyhodnotitelných zveřejněných nástupů spoofingu (kde bylo okno před nástupem čisté, první alarm přišel 10,2 až 39 s po pu
• MODELLED Deterministické, hashované po scénářích, brány SBOM a zlatých výsledků mezi platformami. Orákulum (ExternalDataset): shoda SBOM s oficiálním schématem JSON CycloneDX 1,5 (+ platné identifikátory SPDX) — externí publikovaný standard, nula chyb validace přes celý graf závislostí; část o determinismu FoM / bajtové reprodukovatelnosti zůstává zafixovanou kontrolou vlastní konzistence, takže řádek zůstává MODELLED

Omezení#

Co zpráva samotného běhu uvádí jako nemodelované nebo neověřené:

• Holdover hodin při odepření GNSS je MODELLED, nikoli ověřen proti nezávislé vnější referenci: kontroluje se proti samostatné implementaci v téže kódové základně, nezávislé na testované jednotce, ale není vnějším autoritativním zdrojem. (verifikační matice (docs/MODELLED-RATIONALE.md))
• Odhad stavu palubních hodin je MODELLED, nikoli ověřen proti nezávislé vnější referenci: kontroluje se proti samostatné implementaci v téže kódové základně, nezávislé na testované jednotce, ale není vnějším autoritativním zdrojem. (verifikační matice (docs/MODELLED-RATIONALE.md))
• Detekce spoofingu je MODELLED, nikoli ověřena proti nezávislé vnější referenci: dílčí tvrzení je zkontrolováno externě, ale celá schopnost skládá dohromady části vypočtené z modelu, takže schopnost zůstává vypočtena z modelu. (verifikační matice (docs/MODELLED-RATIONALE.md))
• Reprodukovatelnost a zajištění softwaru je MODELLED, nikoli ověřeno nezávislou referencí: dílčí tvrzení je externě zkontrolováno, ale celá schopnost skládá modelované části, takže schopnost zůstává vypočtená z modelu. (verifikační matice (docs/MODELLED-RATIONALE.md))

Viz také#

• Stránka rodiny: Hodiny, časování a holdover
• Všechny druhy: KINDS.md
• Tematická stránka: CAMPAIGNS.md
• Tematická stránka: RECEIVER-TRUST.md