clock (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#

Ur-holdover mod specifikation; valgfrit Monte Carlo-ensemble (runs > 1).

Én kørsel af scenarios/clock-ensemble.toml opsummeres som: scenario 91d2b6d10d14 | 200 kørsler | kvante-holdover 6600s [6600-6600] p95 8.78e-4ns sikkerhed n/a (intet angreb) | klassisk holdover 844s [220-2130] p95 167.0ns sikkerhed n/a (intet angreb)

Input#

Fra skemaet (kshana kinds --json):

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

Eksemplet scenarios/clock-ensemble.toml angiver blandt andet:

Kør den#

kshana scenarios/clock-ensemble.toml

6 medfølgende scenarier bruger denne type; de øvrige findes i scenarios/.

Hvad den giver#

De skalare resultater af den kørsel, med de enheder, motoren angiver:

Evidens#

MODELLED: rækkerne i verifikationsmatrixen, der nævner denne type.

• MODELLED Den valgfrie [integrity]-sektion i urtypen (clock_integrity::run): ud fra et angivet sted og konstellationsforudindstillinger (geometry::sky_geometry), ved hver integritetsepoke, mens GNSS-tidslinjen ikke er nægtet, snapshot-RAIM (raim::snapshot_ Tests: clock_integrity.rs.
• MODELLED clock_log::read_input: ét parserlag, der omsætter en RINEX-urfil (AS/AR-poster for ét navngivet ur, versionerne 2 og 3,00 til 3,04), en ASCII-fase- eller frekvenslog i TimeLab-stil eller en TAPR TICC-tidsstempel- eller intervallog til en ensartet pha Tests: clock_log_allantools.rs.
• MODELLED clock_log::read_input med formaterne ptp4l, phc2sys, ts2phc, chrony-tracking og chrony-statistics: den loggede offset for en linuxptp-servolinje (ns, linjens eget tidsstempel i klammer, aflæsninger før servoen første gang rapporterer s2 udeladt a
• MODELLED Typen mission-thread: et dokument af faser, hver en af otte registrerede typer, kørt i rækkefølge, hvor 6x6-kovariansen, uret og referencesystemet gives videre efter en angiven regel (carry; inflate, hvid accelerationsstøj over et angivet hul Tests: field_units_global.rs.
• og 1 flere i matricen.

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):

• VALIDATED Allan-/modificeret/Hadamard-afvigelse + identifikation af potenslovsstøj med χ²-konfidensintervaller. Uafhængig reference (ExternalDataset): NIST SP 1065 (Riley) / Stable32-referenceafvigelser på NBS14
• MODELLED Lukket form for vækst i fejl under frit løb + holdover til tærskel; kvanteurklasser. Uafhængig reference (ReferenceImpl): Flertrins clock_state-kovariansrekursion (krydskontrol i samme kodebase); selve kernen for frit-løb-varians og holdover-inversion er eksternt valideret mod scipy (se 'Clock-holdover coast-variance & threshold inversion'). Tallene for holdover pr. klasse ved rødstøjsgulvet forbliver MODELLED
• MODELLED 3-tilstands (fase/frekvens/drift) van Loan-Kalman-ur, Joseph-stabiliseret. Uafhængig reference (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), med F via scipy.linalg.expm og Q via Van-Loan 1978-blokmatrixen — en uafhængig referenceimplementering, der gengiver kshanas fulde filterforløb. Konsistens mellem implementeringer: urfysikken / Allan-kalibreringen er ikke eksternt valideret, så dette forbliver MODELLED. 0,30 ekstern sammenligning, et fund (forbliver MODELLED): på IGS final 30 s-ure fra 11 GPS Blo
• MODELLED Urstøttet χ², RAIM, AGC, SQM sammenlagt sikkerhedskvalitetsmål pr. epoke. Uafhængig reference (ExternalDataset): TEXBAT-scenarieparametre (Humphreys 2012) — karakterisering, ikke fastlåste vektorer. 0,30 ekstern sammenligning, et fund (forbliver MODELLED): på JammerTest 2024 (Bleik; GPL-3.0-data) udløste monitorerne på observabelniveau (urstøttet chi-i-anden, RAIM, løsningsfejl) ingen alarm inden for 10 s af nogen af de 8 evaluerbare publicerede spoofing-starter (hvor vinduet før starten var rent, kom den første alarm 10,2 til 39 s efter pu
• 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

Begrænsninger#

Hvad kørslens egen rapport siger ikke er modelleret eller ikke er valideret:

• Ur-holdover i GNSS-nægtede miljøer er MODELLED, ikke valideret: kontrolleret mod en separat implementering i denne samme kodebase — uafhængig af den enhed, der afprøves, men ikke eksternt autoritativ. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))
• Tilstandsestimering af ombordur er MODELLED, ikke valideret: kontrolleret mod en separat implementering i denne samme kodebase — uafhængig af den enhed, der afprøves, men ikke eksternt autoritativ. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))
• Detektion af spoofing er MODELLED, ikke valideret: en delpåstand kontrolleres eksternt, men hele funktionen sammensættes af modellerede dele, så funktionen forbliver modelleret. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))
• Reproducerbarhed og softwarekvalitetssikring er MODELLED, ikke valideret: en delpåstand kontrolleres eksternt, men hele funktionen sammensættes af modellerede dele, så funktionen forbliver modelleret. (verifikationsmatrix (docs/MODELLED-RATIONALE.md))

Se også#

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