slot-timing (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á#
Slot timing: počet sekund, než volně běžící hodiny opustí ochranný interval časově indexovaného směrovacího nebo úkolovacího slotu (největší absolutní časová chyba, kterou slot toleruje), příspěvek každého členu v tom okamžiku s uvedením dominantního (nejistota opravy, bílý fázový šum, bílý, flickerový, náhodné procházky a náhodného běhu frekvenční šum, zbytkový frekvenční posun, teplota, stárnutí), čas zbývající od poslední opravy a největší interval mezi opravami, který hodiny udrží uvnitř, po odečtení latence opravy. Oscilátor je výchozí hodnota TŘÍDY (csac, uso, dsac, tcxo, ocxo nebo rafs: jedna citovaná Allanova odchylka pro jednu sekundu a předpokládaná podlaha červeného šumu), TELEKOMUNIKAČNÍ PŘEDNASTAVENÍ Z KATALOGOVÉHO LISTU nebo vložený KATALOGOVÝ LIST (maxima Allanovy odchylky proložená jako obálka, plus stárnutí a teplotní koeficient) nebo vložený MEASURED ZÁZNAM FÁZE (jeho překrývající se Allanova odchylka proložená váženou metodou nejmenších čtverců v bázi bílé fáze a frekvenční modulace podle IEEE Std 1139, takže podlaha červeného šumu je naměřená, nikoli předpokládaná). Překročení za nejdelší dobou průměrování, kterou katalogový list nebo záznam podporuje, je označeno jako extrapolované. Volitelná sekce spoofingu přidává ochrannou úroveň časování pro přijímač na oběžné dráze: orbitální rychlost a periodu, jak dlouho může jediný pozemní spoofer družici zasáhnout za přelet, práh monitoru podporovaného hodinami a latenci detekce CUSUM, podmíněnou mez, posun, který spoofer při uvedené maximální rychlosti změny nashromáždí, než družice opustí jeho dosah nebo proběhne nezávislá kontrola, a zda je každá kontrola při kontaktu se zemí nebo přes crosslink na tomto spooferu nezávislá. VALIDATED: inverze holdoveru z proloženého záznamu, držená stranou (held out) na skutečných cesiových hodinách měřených proti vodíkovému maseru (tests/slot_timing_cs5071a_holdout.rs, podmíněno daty); u naměřeného krystalového oscilátoru je predikce držená stranou konzervativní, ale nesplňuje práh, takže případ krystalu je MODELLED. MODELLED: zdroje třídy a katalogového listu, deterministické členy a posouzení spoofingu.
Jeden běh scenarios/slot-timing-ocxo-leo.toml se shrnuje takto: slot-timing (zdroj katalogového listu): ochranný interval 100,0 ns při k=3 je překročen 650,8 s po opravě (zbývá 50,8 s); oprava alespoň každých 645,8 s (133,80 za den); dominantní člen: frekvenční šum náhodné procházky
Vstupy#
Ze schématu (kshana kinds --json):
- Povinná pole:
oscillator,slot - Volitelná pole:
spoofing
Příklad scenarios/slot-timing-ocxo-leo.toml mimo jiné nastavuje:
| Pole | Hodnota | Jednotka |
|---|---|---|
kind |
slot-timing | text |
oscillator.preset |
ocxo | text |
slot.elapsed_since_sync_s |
600 | s |
slot.fix_latency_s |
5 | s |
slot.fix_sigma_ns |
10 | ns |
slot.guard_ns |
100 | ns |
slot.k_sigma |
3 | 1 |
slot.temperature_excursion_k |
2 | K |
spoofing.altitude_km |
550 | km |
spoofing.checks[0].kind |
ground-contact | text |
spoofing.checks[0].revisit_s |
2700 | s |
spoofing.checks[0].sigma_ns |
2 | ns |
Spusťte jej#
kshana scenarios/slot-timing-ocxo-leo.toml
Co poskytuje#
Skalární výsledky tohoto běhu s jednotkami, které engine uvádí:
| Výsledek | Hodnota | Jednotka |
|---|---|---|
evidence.id_rule |
stabilní id řádku matice (ID | text |
evidence.matrix |
docs/VERIFICATION-MATRIX.md | text |
evidence.tier |
MODELLED | text |
oscillator.aging_per_day |
1.5000e-10 | 1/d |
oscillator.flicker_avar |
6.2610e-23 | 1 |
oscillator.q_rr |
0 | 1/s^3 |
oscillator.q_rw |
7.3122e-24 | 1/s |
oscillator.q_wf |
0 | s |
oscillator.sigma_y_1s |
8.0652e-12 | 1 |
oscillator.source |
katalogový list | text |
Popisek výsledku (z enginu): MODELLED — čas, než volně běžící hodiny opustí ochranný interval směrovacího slotu, a četnost oprav, která je udrží uvnitř, ze stacionárního mocninného modelu hodin. Zdroj z katalogového listu je obálka jeho maxim, nikoli měření žádného kusu; zdroj třídy stojí na předpokládané podlaze červeného šumu.
Důkazy#
MODELLED 2 · VALIDATED 1: řádky verifikační matice, které tento druh uvádějí.
- VALIDATED Cesta naměřeného záznamu druhu
slot-timing: překrývající se Allanova odchylka fázového záznamu proložená nezápornou metodou nejmenších čtverců vážených edf v bázi bílé fáze a frekvenční modulace podle IEEE Std 1139 (slot_timing::fit_weighted), Testy: slot_timing_cs5071a_holdout.rs. - MODELLED Druh
slot-timing: predikovaná chyba E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² invertovaná pro překročení, zbývající čas, interval resynchronizace po odečtení latence opravy a počet oprav za den, každý člen uvedený zvlášť s Testy: slot_timing_igs_holdout.rs. - MODELLED orbital_timing::orbital_timing, dosažitelné jako sekce spoofingu druhu
slot-timing: rychlost a perioda kruhové oběžné dráhy, nejdelší doba, po kterou může pozemní spoofer družici zasáhnout za přelet, práh monitoru podporovaného hodinami a latence detekce CUSUM
Řádky, které běh sám procvičil, s orákulem, které matice každému dává (veřejné zdroje jsou tam uvedeny):
- 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
- MODELLED Druh
slot-timing: predikovaná chyba E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² invertovaná pro překročení, zbývající čas, resynchronizaci. Orákulum (InternalConsistency): Uzavřené tvary pro každý člen zvlášť a nezávislé hledání kořene holdover::holdover_seconds; údaje z katalogových listů jsou pojmenované dokumenty (docs/SLOT-TIMING.md). Výchozí hodnota třídy stojí na předpokládané podlaze červeného šumu a zdroj z katalogového listu je obálka maxim, takže ani jedno není měřením žádného kusu - MODELLED orbital_timing::orbital_timing, dosažitelné jako sekce spoofingu druhu
slot-timing: rychlost a perioda kruhové oběžné dráhy, nejdelší doba, po kterou může pozemní spoofer. Orákulum (InternalConsistency): Redukce na stávající ochrannou úroveň časování a uzavřené tvary viditelnosti pro kruhovou oběžnou dráhu a kulovou Zemi. Podmíněno detekcí, jeden pozemský spoofer s uvedenou rychlostí změny, přelet přímo nad hlavou na nerotující Zemi; neověřeno na spoofovaném přijímači na oběžné dráze
Omezení#
Co zpráva samotného běhu uvádí jako nemodelované nebo neověřené:
- frekvenční skoky, vlivy záření a relativistické frekvenční posuny (výsledek
not_modelled[0]) - tepelný model: teplotní výchylka se aplikuje jako skok při opravě (výsledek
not_modelled[1]) - samotný synchronizační protokol: oprava vynuluje chybu na fix_sigma_ns (výsledek
not_modelled[2]) - vůči jaké metrice kolísání má být směrovací slot přijímán; viz docs/SLOT-TIMING.md (výsledek
not_modelled[3]) - MODELLED — čas, než volně běžící hodiny opustí ochranný interval směrovacího slotu, a četnost oprav, která je udrží uvnitř, ze stacionárního mocninného modelu hodin. Zdroj z katalogového listu je obálka jeho maxim, nikoli měření žádného kusu; zdroj třídy stojí na předpokládané podlaze červeného šumu. (výsledek
label) - Oscilátor je výchozí hodnota TŘÍDY (csac, uso, dsac, tcxo, ocxo nebo rafs: jedna citovaná Allanova odchylka pro jednu sekundu a předpokládaná podlaha červeného šumu), TELEKOMUNIKAČNÍ PŘEDNASTAVENÍ Z KATALOGOVÉHO LISTU nebo vložený KATALOGOVÝ LIST (maxima Allanovy odchylky proložená jako obálka, plus stárnutí a teplotní koeficient) nebo vložený MEASURED ZÁZNAM FÁZE (jeho překrývající se Allanova odchylka proložená váženou metodou nejmenších čtverců v bázi bílé fáze a IEEE S (katalog druhů (
kshana kinds --json)) - VALIDATED: inverze holdoveru z proloženého záznamu, držená stranou (held out) na skutečných cesiových hodinách měřených proti vodíkovému maseru (tests/slot_timing_cs5071a_holdout.rs, podmíněno daty); u naměřeného krystalového oscilátoru je predikce držená stranou konzervativní, ale nesplňuje práh, takže případ krystalu je MODELLED. (katalog druhů (
kshana kinds --json)) - MODELLED: zdroje třídy a katalogového listu, deterministické členy a posouzení spoofingu. (katalog druhů (
kshana kinds --json))
Viz také#
- Stránka rodiny: Hodiny, časování a holdover
- Všechny druhy: KINDS.md
- Tematická stránka: LEO-PNT.md
- Tematická stránka: DECEIVED-TIME.md