clock (scenariotype)

Scenariotype i motoren v0.40.0, familie Klokker, tidssynkronisering og holdover. Veiledende: analyseutdata fra et forsknings- og ingeniørverktøy, ikke typegodkjent navigasjonsutstyr og ikke en sikkerhetskritisk tjeneste for menneskeliv. Hver etikett her er motorens eller verifikasjonsmatrisens; en type er MODELLED med mindre matrisen sier noe annet (hvordan en etikett fortjenes: Evidens-avsnittet i README).

Hva den gjør#

Klokkens holdover mot spesifikasjonen; valgfritt Monte Carlo-ensemble (runs > 1).

Én kjøring av scenarios/clock-ensemble.toml oppsummeres som: scenario 91d2b6d10d14 | 200 runs | quantum holdover 6600s [6600-6600] p95 8.78e-4ns security n/a (no attack) | classical holdover 844s [220-2130] p95 167.0ns security n/a (no attack)

Inndata#

Fra skjemaet (kshana kinds --json):

• Obligatoriske felt: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
• Valgfrie felt: runs, integrity

Eksempelet scenarios/clock-ensemble.toml setter blant annet:

Kjør den#

kshana scenarios/clock-ensemble.toml

6 medfølgende scenarioer bruker denne typen; de andre ligger i scenarios/.

Hva den gir#

Skalarresultatene fra den kjøringen, med enhetene motoren oppgir:

Evidens#

MODELLED: radene i verifikasjonsmatrisen som navngir denne typen.

• MODELLED Den valgfrie [integrity]-delen av typen clock (clock_integrity::run): fra et oppgitt sted og konstellasjonsforhåndsinnstillinger (geometry::sky_geometry), ved hver integritetsepoke mens GNSS-tidslinjen ikke er avvist, øyeblikks-RAIM (raim::snapshot_ Tester: clock_integrity.rs.
• MODELLED clock_log::read_input: ett parserlag som gjør en RINEX-klokkefil (AS/AR-poster for én navngitt klokke, versjoner 2 og 3,00 til 3,04), en ASCII-fase- eller frekvenslogg i TimeLab-stil, eller en tidsstempel- eller intervalllogg fra TAPR TICC om til en enhetlig pha Tester: clock_log_allantools.rs.
• MODELLED clock_log::read_input med formatene ptp4l, phc2sys, ts2phc, chrony-tracking og chrony-statistics: den loggede offseten fra en linuxptp-servolinje (ns, linjens eget tidsstempel i klammer, avlesninger før servoen først rapporterer s2 utelatt a
• MODELLED Typen mission-thread: et dokument av faser, hver av dem én av åtte registrerte typer, kjørt i rekkefølge med 6x6-kovariansen, klokken og referansesystemet videreført under en oppgitt regel (carry; inflate, hvit akselerasjonsstøy over et oppgitt gap Tester: field_units_global.rs.
• og 1 til i matrisen.

Radene kjøringen selv brukte, med den uavhengige referansen matrisen gir hver (de offentlige kildene er navngitt der):

• VALIDATED Allan-/modifisert/Hadamard-avvik + identifikasjon av potenslov-støy med χ²-konfidensintervaller. Uavhengig referanse (ExternalDataset): NIST SP 1065 (Riley) / Stable32-referanseavvik på NBS14
• MODELLED Lukket form for vekst i glidefeil + holdover-til-terskel; kvantklokkeklasser. Uavhengig referanse (ReferenceImpl): Rekursjon over kovariansen i flere trinn i clock_state (kontroll mot samme kodebase); kjernen for glidevarians og invertering av holdover er eksternt validert mot scipy (se «Clock-holdover coast-variance & threshold inversion»). Tallene for holdover med rød-støy-gulv per klasse forblir MODELLED
• MODELLED 3-tilstands (fase/frekvens/drift) van Loan-Kalman-klokke, Joseph-stabilisert. Uavhengig referanse (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), med F via scipy.linalg.expm og Q via Van-Loan-blokkmatrisen 1978 — en uavhengig referanseimplementering som gjengir hele banen til Kshanas filter. Konsistens på tvers av implementeringer: klokkefysikken / Allan-kalibreringen er ikke eksternt validert, så dette forblir MODELLED. 0,30 ekstern sammenligning, et funn (forblir MODELLED): på IGS final 30 s-klokker fra 11 GPS Blo
• MODELLED Klokkestøttet χ², RAIM, AGC, SQM sammensatt per epoke til en sikkerhetskvalitetsmåling. Uavhengig referanse (ExternalDataset): TEXBAT-scenarioparametere (Humphreys 2012) — karakterisering, ikke fastlåste vektorer. 0,30 ekstern sammenligning, et funn (forblir MODELLED): på JammerTest 2024 (Bleik; GPL-3.0-data) utløste monitorene på observabelnivå (klokkestøttet kjikvadrat, RAIM, løsningssvikt) ingen alarm innen 10 s av noen av de 8 evaluerbare publiserte spoofing-starttidspunktene (der vinduet før start var rent, kom den første alarmen 10,2 til 39 s etter pu
• MODELLED Deterministisk, scenariohashet, SBOM + gates med gylne verdier på tvers av plattformer. Uavhengig referanse (ExternalDataset): SBOM-overensstemmelse med det offisielle CycloneDX 1,5 JSON Schema (+ gyldige SPDX-identifikatorer), en ekstern publisert standard, null valideringsfeil over hele avhengighetsgrafen; delen om FoM-determinisme / byte-reproduserbarhet er fortsatt en festet selvkonsistenssjekk, så raden forblir MODELLED

Begrensninger#

Hva kjøringens egen rapport sier ikke er modellert eller ikke er validert:

• Klokkens holdover uten GNSS er MODELLED, ikke validert: kontrollert mot en separat implementering i denne samme kodebasen — uavhengig av enheten som testes, men ikke eksternt autoritativ. (verifikasjonsmatrise (docs/MODELLED-RATIONALE.md))
• Tilstandsestimering for klokken om bord er MODELLED, ikke validert: kontrollert mot en separat implementering i denne samme kodebasen — uavhengig av enheten som testes, men ikke eksternt autoritativ. (verifikasjonsmatrise (docs/MODELLED-RATIONALE.md))
• Spoofing-deteksjon er MODELLED, ikke validert: en delpåstand er kontrollert eksternt, men hele funksjonen setter sammen modellerte deler, så funksjonen forblir modellert. (verifikasjonsmatrise (docs/MODELLED-RATIONALE.md))
• Reproduserbarhet og programvarekvalitetssikring er MODELLED, ikke validert: en delpåstand er kontrollert eksternt, men hele funksjonen setter sammen modellerte deler, så funksjonen forblir modellert. (verifikasjonsmatrise (docs/MODELLED-RATIONALE.md))

Se også#

• Familieside: Klokker, tidssynkronisering og holdover
• Alle typer: KINDS.md
• Temaside: CAMPAIGNS.md
• Temaside: RECEIVER-TRUST.md