Maskinoversættelse, ikke gennemgået af en modersmålstalende. Engelsk er referencen.

Sider om scenarietyperRedigér på GitHubKilde: docs/kinds/by-kind/slot-timing.md

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.

Diagrammet, som motoren skriver for scenarios/slot-timing-ocxo-leo.toml, type slot-timing

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å#