slot-timing (scenarietype)
Scenarietype i motoren v0.40.0, familie Ure, tidssynkronisering og holdover. Vejledende: analyseoutput fra et forsknings- og ingeniørværktøj, ikke typegodkendt navigationsudstyr og ikke en sikkerhedskritisk tjeneste (safety-of-life). Hver mærkat her er motorens eller verifikationsmatrixens; en type er MODELLED, medmindre matrixen siger andet (hvordan en mærkat opnås: README'ens afsnit Evidence).
Hvad det gør#
Slottidssynkronisering: sekunder, indtil et frit løbende ur forlader beskyttelsesintervallet for en tidsindekseret routing- eller opgaveslot (den største absolutte tidsfejl, slotten tåler), bidraget fra hvert led på det tidspunkt med det dominerende led nævnt (usikkerhed i tidsfixet, hvid fasestøj, hvid, flicker, random walk og random run i frekvensstøj, resterende frekvensforskydning, temperatur, aldring), den tid, der er tilbage siden det sidste tidsfix, og det største interval mellem tidsfix, der holder uret inden for, netto af latens for tidsfixet. Oscillatoren er en KLASSESTANDARD (csac, uso, dsac, tcxo, ocxo eller rafs: én citeret Allan-deviation ved ét sekund og et antaget gulv med rød støj), en FORUDINDSTILLING FRA ET DATABLAD for telekommunikationstidssynkronisering eller et indlejret DATABLAD (maksima for Allan-deviation tilpasset som en envelope, plus aldring og en temperaturkoefficient) eller en indlejret MEASURED FASEREGISTRERING (dens overlappende Allan-deviation tilpasset ved vægtede mindste kvadrater i basen af hvid fase og IEEE Std 1139-frekvensmodulation, så gulvet med rød støj er målt og ikke antaget). Et brud ud over den længste middelværdiperiode, som databladet eller registreringen understøtter, markeres som ekstrapoleret. Et valgfrit afsnit om spoofing tilføjer beskyttelsesniveauet for tidssynkronisering for en modtager i kredsløb: banehastighed og omløbstid, hvor længe en enkelt spoofer på jorden kan nå satellitten pr. overflyv, gulvet for den urstøttede monitor og CUSUM-detektionslatens, den betingede grænse, det træk, en spoofer ved en angivet maksimal rampehastighed samler, før satellitten forlader dens rækkevidde, eller en uafhængig kontrol kører, og om hver kontrol ved jordkontakt eller krydsforbindelse er uafhængig af den spoofer. VALIDATED: inversionen af holdover ud fra en tilpasset registrering, holdt ude (held out) på et reelt cæsiumur målt mod en brintmaser (tests/slot_timing_cs5071a_holdout.rs, datastyret); på en målt krystaloscillator er den tilbageholdte forudsigelse konservativ, men ikke inden for tærsklen, så krystaltilfældet er MODELLED. MODELLED: klasse- og databladskilder, de deterministiske led og vurderingen af spoofing.
Én kørsel af scenarios/slot-timing-ocxo-leo.toml opsummeres som: slot-timing (databladkilde): beskyttelsesinterval 100,0 ns ved k=3 brydes 650,8 s efter et tidsfix (50,8 s tilbage); tidsfix mindst hvert 645,8 s (133,80 pr. dag); dominerende led: frekvensstøj af typen random walk
Input#
Fra skemaet (kshana kinds --json):
- Påkrævede felter:
oscillator,slot - Valgfrie felter:
spoofing
Eksemplet scenarios/slot-timing-ocxo-leo.toml angiver blandt andet:
| Felt | Værdi | Enhed |
|---|---|---|
kind |
slot-timing | tekst |
oscillator.preset |
ocxo | tekst |
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 | tekst |
spoofing.checks[0].revisit_s |
2700 | s |
spoofing.checks[0].sigma_ns |
2 | ns |
Kør den#
kshana scenarios/slot-timing-ocxo-leo.toml
Hvad den giver#
De skalare resultater af den kørsel, med de enheder, motoren angiver:
| Resultat | Værdi | Enhed |
|---|---|---|
evidence.id_rule |
det stabile id for matrixrækken (kolonnen ID | tekst |
evidence.matrix |
docs/VERIFICATION-MATRIX.md | tekst |
evidence.tier |
MODELLED | tekst |
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 |
datasheet | tekst |
Resultatetiket (motorens egen): MODELLED — tid, indtil et frit løbende ur forlader beskyttelsesintervallet for en routing-slot, og den kadence for tidsfix, der holder det inden for, ud fra en stationær potenslovsmodel for uret. En databladkilde er en envelope af dens maksima, ikke en måling af nogen enhed; en klassekilde hviler på et antaget gulv med rød støj.
Evidens#
MODELLED 2 · VALIDATED 1: rækkerne i verifikationsmatrixen, der nævner denne type.
- VALIDATED Stien for målt registrering i typen
slot-timing: den overlappende Allan-deviation af en faseregistrering tilpasset ved edf-vægtede ikke-negative mindste kvadrater i basen af hvid fase og IEEE Std 1139-frekvensmodulation (slot_timing::fit_weighted), Tests: slot_timing_cs5071a_holdout.rs. - MODELLED Typen
slot-timing: den forudsagte fejl E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² inverteret for bruddet, den resterende tid, intervallet for resynkronisering netto af latens for tidsfixet og tidsfix pr. dag, hvert led specificeret med th Tests: slot_timing_igs_holdout.rs. - MODELLED orbital_timing::orbital_timing, tilgængelig som afsnittet om spoofing i typen
slot-timing: hastighed og omløbstid i cirkulær bane, den længste tid en spoofer på jorden kan nå satellitten pr. overflyv, gulvet for den urstøttede monitor og CUSUM-detektionsl
De rækker, som kørslen selv afprøvede, med den uafhængige reference, som matrixen giver hver (de offentlige kilder er nævnt dér):
- MODELLED Deterministisk, scenarie-hashet, SBOM + gates med golden-filer på tværs af platforme. Uafhængig reference (ExternalDataset): SBOM'ens validering mod det officielle CycloneDX 1,5 JSON-skema (+ gyldige SPDX-identifikatorer) — en ekstern publiceret standard, nul valideringsfejl over hele afhængighedsgrafen; den del, der gælder FoM-determinisme / byte-reproducerbarhed, er fortsat et fastlåst selvkonsistenstjek, så rækken forbliver MODELLED
- MODELLED Typen
slot-timing: den forudsagte fejl E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² inverteret for bruddet, den resterende tid, resynkronisering. Uafhængig reference (InternalConsistency): lukkede former for hvert led alene og den uafhængige rodsøgning holdover::holdover_seconds; databladets tal er de navngivne dokumenter (docs/SLOT-TIMING.md). En klassestandard hviler på et antaget gulv med rød støj, og en databladkilde er en envelope af maksima, så ingen af dem er en måling af nogen enhed - MODELLED orbital_timing::orbital_timing, tilgængelig som afsnittet om spoofing i typen
slot-timing: hastighed og omløbstid i cirkulær bane, den længste tid en spoofer på jorden kan n. Uafhængig reference (InternalConsistency): reduktion til det eksisterende beskyttelsesniveau for tidssynkronisering og de lukkede former for synlighed i cirkulær bane og med kugleformet jord. Betinget af detektion, én terrestrisk spoofer ved en angivet rampehastighed, et overflyv lige over hovedet på en ikke-roterende jord; ikke valideret på en spoofet modtager i kredsløb
Begrænsninger#
Hvad kørslens egen rapport siger ikke er modelleret eller ikke er valideret:
- frekvensspring, strålingseffekter og relativistiske frekvensforskydninger (resultat
not_modelled[0]) - en termisk model: temperaturudsvinget anvendes som et trin ved tidsfixet (resultat
not_modelled[1]) - selve synkroniseringsprotokollen: et tidsfix nulstiller fejlen til fix_sigma_ns (resultat
not_modelled[2]) - hvilken metrik for wander en routing-slot bør accepteres mod; se docs/SLOT-TIMING.md (resultat
not_modelled[3]) - MODELLED — tid, indtil et frit løbende ur forlader beskyttelsesintervallet for en routing-slot, og den kadence for tidsfix, der holder det inden for, ud fra en stationær potenslovsmodel for uret. En databladkilde er en envelope af dens maksima, ikke en måling af nogen enhed; en klassekilde hviler på et antaget gulv med rød støj. (resultat
label) - Oscillatoren er en KLASSESTANDARD (csac, uso, dsac, tcxo, ocxo eller rafs: én citeret Allan-deviation ved ét sekund og et antaget gulv med rød støj), en FORUDINDSTILLING FRA ET DATABLAD for telekommunikationstidssynkronisering eller et indlejret DATABLAD (maksima for Allan-deviation tilpasset som en envelope, plus aldring og en temperaturkoefficient) eller en indlejret MEASURED FASEREGISTRERING (dens overlappende Allan-deviation tilpasset ved vægtede mindste kvadrater i basen af hvid fase og IEEE S (typekatalog (
kshana kinds --json)) - VALIDATED: inversionen af holdover ud fra en tilpasset registrering, holdt ude (held out) på et reelt cæsiumur målt mod en brintmaser (tests/slot_timing_cs5071a_holdout.rs, datastyret); på en målt krystaloscillator er den tilbageholdte forudsigelse konservativ, men ikke inden for tærsklen, så krystaltilfældet er MODELLED. (typekatalog (
kshana kinds --json)) - MODELLED: klasse- og databladskilder, de deterministiske led og vurderingen af spoofing. (typekatalog (
kshana kinds --json))
Se også#
- Familieside: Ure, tidssynkronisering og holdover
- Alle typer: KINDS.md
- Emneside: LEO-PNT.md
- Emneside: DECEIVED-TIME.md