Machinevertaling, niet beoordeeld door een moedertaalspreker. Engels is de referentie.

Pagina's per scenariotypeBewerken op GitHubBron: docs/kinds/by-kind/clock.md

clock (scenariokind)

Scenariokind van de engine v0.40.0, familie Klokken, tijdsynchronisatie en holdover. Adviserend: analyse-uitvoer van een onderzoeks- en engineeringhulpmiddel, geen typegoedgekeurde navigatieapparatuur en geen veiligheidskritieke dienst. Elk label hier is dat van de engine of van de verificatiematrix; een kind is MODELLED tenzij de matrix anders zegt (hoe een label wordt verdiend: de sectie Evidence van de README).

Wat het doet#

Klok-holdover tegenover de specificatie; optioneel Monte-Carlo-ensemble (runs > 1).

Eén run van scenarios/clock-ensemble.toml vat samen als: 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)

Invoer#

Uit het schema (kshana kinds --json):

  • Verplichte velden: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Optionele velden: runs, integrity

Het voorbeeld scenarios/clock-ensemble.toml stelt onder meer in:

Veld Waarde Eenheid
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s tekst
clock_classical.provenance Microchip SA65 / SA.45s CSAC-datasheet sigma_y(1s)=3e-10; q_ tekst
clock_classical.q_rw 0 1/s
clock_classical.q_wf 9.0000e-20 s^2/s
clock_classical.y0 5.0000e-10 1
clock_quantum.flicker_floor 1.0000e-16 1
clock_quantum.id optical-sr-lattice tekst
clock_quantum.provenance Optische strontiumroosterklok, op de ruimte gericht doel sigma_y tekst
clock_quantum.q_rw 0 1/s
clock_quantum.q_wf 1.0000e-30 s^2/s
clock_quantum.y0 5.0000e-17 1

Uitvoeren#

kshana scenarios/clock-ensemble.toml

6 meegeleverde scenario's gebruiken deze soort; de andere staan in scenarios/.

Wat het oplevert#

De scalaire resultaten van die run, met de eenheden die de engine noemt:

Resultaat Waarde Eenheid
classical.availability.mean 0.295402 1
classical.availability.p05 0.115118 1
classical.availability.p50 0.242718 1
classical.availability.p95 0.680999 1
classical.filter_health.consistent true vlag
classical.filter_health.nees_chi2_lower_95 1.142439 1
classical.filter_health.nees_chi2_upper_95 3.092704 1
classical.filter_health.nees_mean 1.807227 1
classical.filter_health.nis_chi2_lower_95 0.912528 1
classical.filter_health.nis_chi2_upper_95 1.091418 1
De grafiek die de engine schrijft voor scenarios/clock-ensemble.toml, kind clock

Bewijs#

MODELLED: de rijen van de verificatiematrix die dit type noemen.

  • MODELLED De optionele sectie [integrity] van het kind clock (clock_integrity::run): vanuit een vermelde locatie en constellatievoorinstellingen (geometry::sky_geometry), bij elk integriteitstijdstip zolang de GNSS-tijdlijn niet geweigerd wordt, snapshot-RAIM (raim::snapshot_ Tests: clock_integrity.rs.
  • MODELLED clock_log::read_input: één parserlaag die een RINEX-klokbestand (AS/AR-records van één benoemde klok, versies 2 en 3,00 tot 3,04), een fase- of frequentielog in TimeLab-stijl ASCII, of een TAPR TICC-tijdstempel- of intervallog omzet in een uniforme pha Tests: clock_log_allantools.rs.
  • MODELLED clock_log::read_input met de formaten ptp4l, phc2sys, ts2phc, chrony-tracking en chrony-statistics: de gelogde offset van een linuxptp-servoregel (ns, de eigen tussen haakjes geplaatste tijdstempel van de regel, metingen voordat de servo voor het eerst s2 meldt weggelaten a
  • MODELLED De soort mission-thread: een document met fasen, elk een van acht geregistreerde soorten, in volgorde uitgevoerd, waarbij de 6x6-covariantie, de klok en het referentiestelsel worden doorgegeven volgens een vermelde regel (carry; inflate, witte versnellingsruis over een vermelde onderbreking Tests: field_units_global.rs.
  • en 1 meer in de matrix.

De rijen die de run zelf heeft beproefd, met de onafhankelijke referentie die de matrix aan elk geeft (de openbare bronnen worden daar genoemd):

  • VALIDATED Allan-/gemodificeerde/Hadamard-deviatie + machtswetruisidentificatie met χ²-betrouwbaarheidsintervallen. Onafhankelijke referentie (ExternalDataset): NIST SP 1065 (Riley) / referentiedeviaties van Stable32 op NBS14
  • MODELLED Gesloten-vorm-groei van de driftfout tijdens coasting + holdover-tot-drempel; kwantumklasseklokken. Onafhankelijke referentie (ReferenceImpl): Recursie van de covariantie van clock_state in meerdere stappen (kruiscontrole binnen dezelfde codebase); de onderliggende kernel voor coast-variantie en holdover-inversie is extern getoetst tegen scipy (zie 'Clock-holdover coast-variance & threshold inversion'). De holdovercijfers per klasse met rode-ruisbodem blijven MODELLED
  • MODELLED 3-toestanden (fase/frequentie/drift) van-Loan-Kalmanklok, Joseph-gestabiliseerd. Onafhankelijke referentie (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), met F via scipy.linalg.expm en Q via de Van-Loan-blokmatrix van 1978 — een onafhankelijke referentie-implementatie die het volledige filtertraject van kshana reproduceert. Consistentie tussen implementaties: de klokfysica en de Allan-kalibratie zijn niet extern getoetst, dus dit blijft MODELLED. 0,30 externe vergelijking, een bevinding (blijft MODELLED): op IGS final 30 s-klokken van 11 GPS Blo
  • MODELLED Klokondersteunde χ², RAIM, AGC, SQM, per tijdstip gefuseerde veiligheidskwaliteitsmaat. Onafhankelijke referentie (ExternalDataset): TEXBAT-scenarioparameters (Humphreys 2012) — karakterisering, geen vastgezette vectoren. 0,30 externe vergelijking, een bevinding (blijft MODELLED): op JammerTest 2024 (Bleik; GPL-3.0-data) gaven de monitors op waarnemingsniveau (klokondersteunde chikwadraat, RAIM, oplossingsfout) geen alarm binnen 10 s van een van de 8 evalueerbare gepubliceerde spoofingbegintijden (waar het venster vóór het begin schoon was, kwam het eerste alarm 10,2 tot 39 s na de pu
  • MODELLED Deterministisch, scenario-gehasht, SBOM + gouden poorten voor meerdere platforms. Onafhankelijke referentie (ExternalDataset): formaatcontrole van de SBOM tegen het officiële CycloneDX 1,5 JSON Schema (+ geldige SPDX-identificatoren) — een externe gepubliceerde standaard, nul validatiefouten over de volledige afhankelijkheidsgraaf; het onderdeel determinisme van de FoM en byte-reproduceerbaarheid blijft een vastgepinde zelfconsistentiecontrole, dus de rij blijft MODELLED

Beperkingen#

Wat het eigen rapport van de run zegt dat niet is gemodelleerd of niet extern getoetst is:

  • Klok-holdover bij GNSS-uitval is MODELLED, niet extern getoetst: gecontroleerd tegen een afzonderlijke implementatie in dezelfde codebase — onafhankelijk van de geteste eenheid, maar niet extern gezaghebbend. (verificatiematrix (docs/MODELLED-RATIONALE.md))
  • Schatting van de toestand van de boordklok is MODELLED, niet extern getoetst: gecontroleerd tegen een afzonderlijke implementatie in dezelfde codebase — onafhankelijk van de geteste eenheid, maar niet extern gezaghebbend. (verificatiematrix (docs/MODELLED-RATIONALE.md))
  • Spoofingdetectie is MODELLED, niet extern getoetst: een deelclaim wordt extern gecontroleerd, maar de hele mogelijkheid is samengesteld uit gemodelleerde onderdelen, dus de mogelijkheid blijft gemodelleerd. (verificatiematrix (docs/MODELLED-RATIONALE.md))
  • Reproduceerbaarheid en softwarewaarborging is MODELLED, niet extern getoetst: een deelclaim wordt extern gecontroleerd, maar de hele mogelijkheid is samengesteld uit gemodelleerde onderdelen, dus de mogelijkheid blijft gemodelleerd. (verificatiematrix (docs/MODELLED-RATIONALE.md))

Zie ook#