Maschinelle Übersetzung, nicht von einem Muttersprachler geprüft. Englisch ist die maßgebliche Fassung.

Seiten zu den SzenariotypenAuf GitHub bearbeitenQuelle: docs/kinds/by-kind/clock.md

clock (Szenariotyp)

Szenariotyp der Engine v0.40.0, Familie Uhren, Zeitgebung und Holdover. Nur beratend: Analyseausgabe eines Forschungs- und Engineering-Werkzeugs, keine typzugelassene Navigationsausrüstung und kein Safety-of-Life-Dienst. Jede Kennzeichnung hier stammt von der Engine oder von der Verifikationsmatrix; ein Typ ist MODELLED, sofern die Matrix nichts anderes angibt (wie eine Kennzeichnung erworben wird: Abschnitt „Evidence“ der README).

Was es tut#

Uhren-Holdover gegen Spezifikation; optionales Monte-Carlo-Ensemble (runs > 1).

Ein Lauf von scenarios/clock-ensemble.toml ergibt zusammengefasst: Szenario 91d2b6d10d14 | 200 Läufe | Quanten-Holdover 6600s [6600-6600] p95 8.78e-4ns Sicherheit n/a (kein Angriff) | klassischer Holdover 844s [220-2130] p95 167.0ns Sicherheit n/a (kein Angriff)

Eingaben#

Aus dem Schema (kshana kinds --json):

  • Pflichtfelder: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Optionale Felder: runs, integrity

Das Beispiel scenarios/clock-ensemble.toml setzt unter anderem:

Feld Wert Einheit
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s Text
clock_classical.provenance Microchip SA65 / SA.45s CSAC Datenblatt sigma_y(1s)=3e-10; q_ Text
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 Text
clock_quantum.provenance Optische Strontium-Gitteruhr, weltraumtaugliches Ziel sigma_y Text
clock_quantum.q_rw 0 1/s
clock_quantum.q_wf 1.0000e-30 s^2/s
clock_quantum.y0 5.0000e-17 1

Ausführen#

kshana scenarios/clock-ensemble.toml

6 mitgelieferte Szenarien verwenden diese Art; die übrigen stehen in scenarios/.

Was es liefert#

Die skalaren Ergebnisse dieses Laufs, mit den Einheiten, die die Engine angibt:

Ergebnis Wert Einheit
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 Flag
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
Das Diagramm, das die Engine für scenarios/clock-ensemble.toml schreibt, Typ clock

Nachweise#

MODELLED: die Zeilen der Verifikationsmatrix, die diese Art nennen.

  • MODELLED Der optionale Abschnitt [integrity] des Typs clock (clock_integrity::run): aus einem festgelegten Standort und Konstellations-Voreinstellungen (geometry::sky_geometry), zu jeder Integritätsepoche, solange die GNSS-Zeitreihe nicht gesperrt ist, Snapshot-RAIM (raim::snapshot_ Tests: clock_integrity.rs.
  • MODELLED clock_log::read_input: eine Parser-Schicht, die eine RINEX-Uhrendatei (AS/AR-Einträge einer benannten Uhr, Versionen 2 und 3,00 bis 3,04), ein ASCII-Phasen- oder Frequenzprotokoll im TimeLab-Stil oder ein TAPR-TICC-Zeitstempel- oder Intervallprotokoll in eine einheitliche Pha Tests: clock_log_allantools.rs.
  • MODELLED clock_log::read_input mit den Formaten ptp4l, phc2sys, ts2phc, chrony-tracking und chrony-statistics: der protokollierte Offset einer linuxptp-Servo-Zeile (ns, der eigene eingeklammerte Zeitstempel der Zeile, Messwerte, bevor der Servo erstmals s2 meldet, entfallen a
  • MODELLED Die Art mission-thread: ein Dokument aus Phasen, jede eine von acht registrierten Arten, der Reihe nach ausgeführt, wobei die 6x6-Kovarianz, die Uhr und das Bezugssystem nach einer genannten Regel weitergegeben werden (carry; inflate, weißes Beschleunigungsrauschen über eine genannte Lücke Tests: field_units_global.rs.
  • und 1 weitere in der Matrix.

Die Zeilen, die der Lauf selbst ausgeübt hat, mit der unabhängigen Referenz, die die Matrix jeder gibt (die öffentlichen Quellen sind dort genannt):

  • VALIDATED Allan-/modifizierte/Hadamard-Abweichung + Potenzgesetz-Rauschidentifikation mit χ²-Konfidenzintervallen. Unabhängige Referenz (ExternalDataset): NIST SP 1065 (Riley) / Stable32-Referenzabweichungen auf NBS14
  • MODELLED Geschlossene Formel für das Wachstum des Auslauffehlers + Holdover bis zum Schwellenwert; Quantenuhr-Klassen. Unabhängige Referenz (ReferenceImpl): Mehrschritt-Kovarianzrekursion von clock_state (Gegenprüfung innerhalb derselben Codebasis); der zugrunde liegende Kern für Auslaufvarianz und Holdover-Inversion ist extern gegen scipy validiert (siehe „Clock-holdover coast-variance & threshold inversion“). Die Holdover-Werte je Klasse mit Rotrauschboden bleiben MODELLED
  • MODELLED 3-Zustands-Van-Loan-Kalman-Uhr (Phase/Frequenz/Drift), Joseph-stabilisiert. Unabhängige Referenz (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), mit F über scipy.linalg.expm und Q über die Van-Loan-1978-Blockmatrix – eine unabhängige Referenzimplementierung, die die vollständige Filtertrajektorie von kshana reproduziert. Konsistenz über Implementierungen hinweg: Die Uhrenphysik / Allan-Kalibrierung ist nicht extern validiert, daher bleibt dies MODELLED. 0,30 externer Vergleich, ein Befund (bleibt MODELLED): auf IGS-Final-30-s-Uhren von 11 GPS Blo
  • MODELLED Uhrengestütztes χ², RAIM, AGC, SQM, fusioniert zu einer Sicherheits-Gütezahl je Epoche. Unabhängige Referenz (ExternalDataset): TEXBAT-Szenarioparameter (Humphreys 2012) – Charakterisierung, keine festgelegten Vektoren. 0,30 externer Vergleich, ein Befund (bleibt MODELLED): bei JammerTest 2024 (Bleik; GPL-3.0-Daten) lösten die Monitore auf Beobachtungsebene (uhrengestütztes Chi-Quadrat, RAIM, Lösungsausfall) innerhalb von 10 s bei keinem der 8 auswertbaren veröffentlichten Spoofing-Einsätze Alarm aus (wo das Fenster vor dem Einsatz sauber war, kam der erste Alarm 10,2 bis 39 s nach dem pu
  • MODELLED Deterministisch, szenario-gehasht, SBOM- und plattformübergreifende Golden-Gates. Unabhängige Referenz (ExternalDataset): SBOM-Übereinstimmung mit dem offiziellen CycloneDX-1,5-JSON-Schema (+ gültige SPDX-Kennungen) — ein externer veröffentlichter Standard, null Validierungsfehler über den gesamten Abhängigkeitsgraphen; der Teil FoM-Determinismus / Byte-Reproduzierbarkeit bleibt eine festgelegte Selbstkonsistenzprüfung, daher bleibt die Zeile MODELLED

Einschränkungen#

Was der eigene Bericht des Laufs als nicht modelliert oder nicht validiert nennt:

  • GNSS-gesperrter Uhren-Holdover ist MODELLED, nicht validiert: gegen eine separate Implementierung in derselben Codebasis geprüft – unabhängig von der geprüften Einheit, aber extern nicht maßgeblich. (Verifikationsmatrix (docs/MODELLED-RATIONALE.md))
  • Die Zustandsschätzung der Bordzeit-Uhr ist MODELLED, nicht validiert: gegen eine separate Implementierung in derselben Codebasis geprüft – unabhängig von der geprüften Einheit, aber extern nicht maßgeblich. (Verifikationsmatrix (docs/MODELLED-RATIONALE.md))
  • Spoofing-Erkennung ist MODELLED, nicht validiert: eine Teilaussage ist extern geprüft, aber die gesamte Fähigkeit setzt sich aus modellierten Teilen zusammen, daher bleibt die Fähigkeit modelliert. (Verifikationsmatrix (docs/MODELLED-RATIONALE.md))
  • Reproduzierbarkeit und Software-Assurance ist MODELLED, nicht validiert: Eine Teilbehauptung ist extern geprüft, aber die gesamte Fähigkeit setzt sich aus modellierten Teilen zusammen, daher bleibt die Fähigkeit modelliert. (Verifikationsmatrix (docs/MODELLED-RATIONALE.md))

Siehe auch#