Traduction automatique, non relue par un locuteur natif. L'anglais fait foi.

Pages des types de scénarioModifier sur GitHubSource : docs/kinds/by-kind/clock.md

clock (type de scénario)

Type de scénario du moteur v0.40.0, famille Horloges, synchronisation temporelle et holdover. À titre consultatif : résultat d'analyse issu d'un outil de recherche et d'ingénierie, et non un équipement de navigation homologué ni un service de sauvegarde de la vie humaine. Chaque étiquette ici est celle du moteur ou de la matrice de vérification ; un type de scénario est MODELLED sauf indication contraire de la matrice (comment une étiquette s'obtient : section Evidence du README).

Ce qu'il fait#

Holdover d'horloge par rapport à la spécification ; ensemble Monte-Carlo facultatif (runs > 1).

Une exécution de scenarios/clock-ensemble.toml se résume ainsi : 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)

Entrées#

D'après le schéma (kshana kinds --json) :

  • Champs obligatoires : seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Champs facultatifs : runs, integrity

L'exemple scenarios/clock-ensemble.toml définit, entre autres :

Champ Valeur Unité
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s texte
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ texte
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 texte
clock_quantum.provenance Strontium optical lattice clock, space-oriented goal sigma_y texte
clock_quantum.q_rw 0 1/s
clock_quantum.q_wf 1.0000e-30 s^2/s
clock_quantum.y0 5.0000e-17 1

L'exécuter#

kshana scenarios/clock-ensemble.toml

6 scénarios fournis utilisent ce type ; les autres se trouvent dans scenarios/.

Ce qu'il donne#

Les résultats scalaires de cette exécution, avec les unités que le moteur indique :

Résultat Valeur Unité
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 indicateur
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
Le graphique que le moteur écrit pour scenarios/clock-ensemble.toml, type de scénario clock

Preuves#

MODELLED : les lignes de la matrice de vérification qui nomment ce type de scénario.

  • MODELLED La section facultative [integrity] du type de scénario clock (clock_integrity::run) : à partir d'un site indiqué et de préréglages de constellation (geometry::sky_geometry), à chaque époque d'intégrité tant que la chronologie GNSS n'est pas refusée, RAIM instantané (raim::snapshot_ Tests : clock_integrity.rs.
  • MODELLED clock_log::read_input : une couche d'analyse unique qui transforme un fichier d'horloge RINEX (enregistrements AS/AR d'une horloge nommée, versions 2 et 3,00 à 3,04), un journal ASCII de phase ou de fréquence de type TimeLab, ou un journal d'horodatages ou d'intervalles TAPR TICC en un fichier uniforme de pha Tests : clock_log_allantools.rs.
  • MODELLED clock_log::read_input avec les formats ptp4l, phc2sys, ts2phc, chrony-tracking et chrony-statistics : le décalage consigné d'une ligne d'asservissement linuxptp (ns, l'horodatage entre crochets propre à la ligne, les mesures antérieures au premier rapport de l'asservissement s2 écartées a
  • MODELLED Le type mission-thread : un document de phases, chacune d'un des huit types enregistrés, exécutées dans l'ordre avec la covariance 6x6, l'horloge et le référentiel transmis selon une règle déclarée (carry ; inflate, bruit d'accélération blanc sur un intervalle déclaré Tests : field_units_global.rs.
  • et 1 autre dans la matrice.

Les lignes que l'exécution elle-même a exercées, avec la référence indépendante que la matrice donne pour chacune (les sources publiques y sont nommées) :

  • VALIDATED Écart-type d'Allan / modifié / d'Hadamard + identification du bruit en loi de puissance avec intervalles de confiance en χ². Référence indépendante (ExternalDataset) : NIST SP 1065 (Riley) / écarts-types de référence de Stable32 sur NBS14
  • MODELLED Croissance de l'erreur de dérive en forme fermée + holdover jusqu'au seuil ; classes d'horloges quantiques. Référence indépendante (ReferenceImpl) : récurrence de covariance multi-pas de clock_state (recoupement au sein de la même base de code) ; le noyau sous-jacent de variance de dérive et d'inversion du holdover est validé en externe par rapport à scipy (voir « Clock-holdover coast-variance & threshold inversion »). Les chiffres de holdover par classe au plancher de bruit rouge restent MODELLED
  • MODELLED Horloge de Kalman de van Loan à 3 états (phase/fréquence/dérive), stabilisée de Joseph. Référence indépendante (ReferenceImpl) : filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), avec F via scipy.linalg.expm et Q via la matrice par blocs de Van Loan 1978 — une implémentation de référence indépendante qui reproduit toute la trajectoire du filtre de kshana. Cohérence entre implémentations : la physique de l'horloge et l'étalonnage d'Allan ne sont pas validés en externe, ce qui laisse cela MODELLED. 0,30 comparaison externe, un constat (reste MODELLED) : sur les horloges IGS finales de 30 s de 11 GPS Blo
  • MODELLED χ² assisté par l'horloge, RAIM, AGC, SQM fusionnés en un indice de mérite de sécurité par époque. Référence indépendante (ExternalDataset) : paramètres de scénario TEXBAT (Humphreys 2012) — caractérisation, et non vecteurs figés. 0,30 comparaison externe, un constat (reste MODELLED) : sur JammerTest 2024 (Bleik ; données GPL-3.0) les moniteurs de niveau observable (khi-deux assisté par l'horloge, RAIM, échec de résolution) n'ont déclenché aucune alarme dans les 10 s suivant l'un des 8 débuts de leurrage publiés évaluables (là où la fenêtre précédant le début était propre, la première alarme est venue 10,2 à 39 s après le pu
  • MODELLED Déterministe, hachée par scénario, avec des barrières SBOM + références d'or multiplateformes. Référence indépendante (ExternalDataset) : respect du schéma JSON officiel CycloneDX 1,5 par la SBOM (+ identifiants SPDX valides) — une norme publiée externe, zéro erreur de validation sur tout le graphe de dépendances ; la partie déterminisme du FoM / reproductibilité à l'octet près reste un contrôle d'autocohérence figé, de sorte que la ligne reste MODELLED

Limites#

Ce que le rapport propre à l'exécution dit n'être pas modélisé ou pas validé :

  • Le holdover d'horloge sans GNSS est MODELLED, et non validé : vérifié par rapport à une implémentation distincte de cette même base de code — indépendante de l'unité testée, mais sans autorité externe. (matrice de vérification (docs/MODELLED-RATIONALE.md))
  • L'estimation de l'état de l'horloge embarquée est MODELLED, et non validée : vérifiée par rapport à une implémentation distincte de cette même base de code — indépendante de l'unité testée, mais sans autorité externe. (matrice de vérification (docs/MODELLED-RATIONALE.md))
  • La détection du leurrage est MODELLED, et non validée : une sous-affirmation est vérifiée en externe, mais la capacité entière compose des éléments modélisés, de sorte que la capacité reste modélisée. (matrice de vérification (docs/MODELLED-RATIONALE.md))
  • La reproductibilité et l'assurance logicielle sont MODELLED, et non validées : une sous-affirmation est vérifiée de l'extérieur, mais la capacité entière compose des éléments modélisés, de sorte qu'elle reste modélisée. (matrice de vérification (docs/MODELLED-RATIONALE.md))

Voir aussi#