slot-timing (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#

Synchronisation d'un créneau : nombre de secondes avant qu'une horloge en marche libre ne sorte de la marge de garde d'un créneau d'acheminement ou d'affectation indexé sur le temps (l'erreur de temps absolue maximale que le créneau tolère), contribution de chaque terme à cet instant avec le terme dominant nommé (incertitude de recalage, bruit blanc de phase, bruit de fréquence blanc, de scintillation, de marche aléatoire et de course aléatoire, décalage de fréquence résiduel, température, vieillissement), temps restant depuis le dernier recalage, et plus grand intervalle de recalage qui maintient l'horloge dans la marge, net de la latence du recalage. L'oscillateur est une valeur par défaut de CLASSE (csac, uso, dsac, tcxo, ocxo ou rafs : un écart-type d'Allan à une seconde cité et un plancher de bruit rouge supposé), un PRÉRÉGLAGE DE FICHE TECHNIQUE de synchronisation télécom ou une FICHE TECHNIQUE en ligne (maxima d'écart-type d'Allan ajustés comme une enveloppe, plus le vieillissement et un coefficient de température), ou un ENREGISTREMENT DE PHASE MEASURED en ligne (son écart-type d'Allan chevauchant ajusté par moindres carrés pondérés dans la base du bruit blanc de phase et du bruit de modulation de fréquence de l'IEEE Std 1139, de sorte que le plancher de bruit rouge est mesuré et non supposé). Un dépassement au-delà du plus long temps de moyennage que la fiche technique ou l'enregistrement permet est signalé comme extrapolé. Une section facultative de leurrage ajoute le niveau de protection de la synchronisation temporelle pour un récepteur en orbite : vitesse et période orbitales, durée pendant laquelle un seul leurre au sol peut atteindre le satellite par passage, plancher du moniteur assisté par l'horloge et latence de détection CUSUM, borne conditionnelle, écart qu'accumule un leurre à un taux de rampe maximal donné avant que le satellite ne quitte sa portée ou qu'une vérification indépendante ne s'exécute, et indication si chaque vérification par contact au sol ou par liaison croisée est indépendante de ce leurre. VALIDATED : l'inversion de holdover à partir d'un enregistrement ajusté, mise de côté sur une vraie horloge au césium mesurée par rapport à un maser à hydrogène (tests/slot_timing_cs5071a_holdout.rs, conditionné par les données) ; sur un oscillateur à quartz mesuré, la prédiction mise de côté est prudente mais n'atteint pas le seuil, de sorte que le cas du quartz est MODELLED. MODELLED : les sources de classe et de fiche technique, les termes déterministes et l'évaluation du leurrage.

Une exécution de scenarios/slot-timing-ocxo-leo.toml se résume ainsi : slot-timing (source fiche technique) : marge de garde 100,0 ns à k=3 franchie 650,8 s après un recalage (50,8 s restantes) ; recalage au moins toutes les 645,8 s (133,80 par jour) ; terme dominant : bruit de fréquence de marche aléatoire

Entrées#

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

• Champs obligatoires : oscillator, slot
• Champs facultatifs : spoofing

L'exemple scenarios/slot-timing-ocxo-leo.toml définit, entre autres :

L'exécuter#

kshana scenarios/slot-timing-ocxo-leo.toml

Ce qu'il donne#

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

Libellé du résultat (celui du moteur) : MODELLED — temps avant qu'une horloge en marche libre ne sorte de la marge de garde d'un créneau d'acheminement, et cadence de recalage qui la maintient dans la marge, à partir d'un modèle d'horloge stationnaire en loi de puissance. Une source de fiche technique est une enveloppe de ses maxima, et non la mesure d'une unité quelconque ; une source de classe repose sur un plancher de bruit rouge supposé.

Preuves#

MODELLED 2 · VALIDATED 1 : les lignes de la matrice de vérification qui nomment ce type.

• VALIDATED Le chemin d'enregistrement mesuré du type slot-timing : l'écart-type d'Allan chevauchant d'un enregistrement de phase ajusté par moindres carrés non négatifs pondérés par edf dans la base du bruit blanc de phase et du bruit de modulation de fréquence de l'IEEE Std 1139 (slot_timing::fit_weighted), Tests : slot_timing_cs5071a_holdout.rs.
• MODELLED Le type slot-timing : l'erreur prédite E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² inversée pour le dépassement, le temps restant, l'intervalle de resynchronisation net de la latence du recalage et les recalages par jour, chaque terme détaillé avec th Tests : slot_timing_igs_holdout.rs.
• MODELLED orbital_timing::orbital_timing, accessible comme section de leurrage du type slot-timing : vitesse et période en orbite circulaire, durée maximale pendant laquelle un leurre au sol peut atteindre le satellite par passage, plancher du moniteur assisté par l'horloge et latence de détection CUSUM l

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

• 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
• MODELLED Le type slot-timing : l'erreur prédite E(t) = k·√(σ₀² + σ_x²(t)) + (|y₀| + |c_T·ΔT|)·t + ½|D|t² inversée pour le dépassement, le temps restant, la resynchronisati. Référence indépendante (InternalConsistency) : formes fermées pour chaque terme seul et recherche de racine indépendante holdover::holdover_seconds ; les valeurs de fiche technique sont les documents nommés (docs/SLOT-TIMING.md). Une valeur de classe par défaut repose sur un plancher de bruit rouge supposé et une source de fiche technique est une enveloppe de maxima, de sorte qu'aucune n'est la mesure d'une unité quelconque
• MODELLED orbital_timing::orbital_timing, accessible comme section de leurrage du type slot-timing : vitesse et période en orbite circulaire, durée maximale pendant laquelle un leurre au sol peut atteindre le satellite par passage, plancher du moniteur assisté par l'horloge et latence de détection CUSUM l. Référence indépendante (InternalConsistency) : réduction au niveau de protection de la synchronisation temporelle existant et aux formes fermées de visibilité pour une orbite circulaire et une Terre sphérique. Conditionnel à la détection, un leurre terrestre à un taux de rampe donné, un passage au zénith sur une Terre non tournante ; non validé sur un récepteur leurré en orbite

Limites#

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

• sauts de fréquence, effets des rayonnements et décalages de fréquence relativistes (résultat not_modelled[0])
• un modèle thermique : l'excursion de température est appliquée comme un échelon au moment du recalage (résultat not_modelled[1])
• le protocole de synchronisation lui-même : un recalage ramène l'erreur à fix_sigma_ns (résultat not_modelled[2])
• la métrique de dérive selon laquelle un créneau d'acheminement devrait être accepté ; voir docs/SLOT-TIMING.md (résultat not_modelled[3])
• MODELLED — temps avant qu'une horloge en marche libre ne sorte de la marge de garde d'un créneau d'acheminement, et cadence de recalage qui la maintient dans la marge, à partir d'un modèle d'horloge stationnaire en loi de puissance. Une source de fiche technique est une enveloppe de ses maxima, et non la mesure d'une unité quelconque ; une source de classe repose sur un plancher de bruit rouge supposé. (résultat label)
• L'oscillateur est une valeur par défaut de CLASSE (csac, uso, dsac, tcxo, ocxo ou rafs : un écart-type d'Allan à une seconde cité et un plancher de bruit rouge supposé), un PRÉRÉGLAGE DE FICHE TECHNIQUE de synchronisation télécom ou une FICHE TECHNIQUE en ligne (maxima d'écart-type d'Allan ajustés comme une enveloppe, plus le vieillissement et un coefficient de température), ou un ENREGISTREMENT DE PHASE MEASURED en ligne (son écart-type d'Allan chevauchant ajusté par moindres carrés pondérés dans la base du bruit blanc de phase et de l'IEEE S (catalogue des types (kshana kinds --json))
• VALIDATED : l'inversion de holdover à partir d'un enregistrement ajusté, mise de côté sur une vraie horloge au césium mesurée par rapport à un maser à hydrogène (tests/slot_timing_cs5071a_holdout.rs, conditionné par les données) ; sur un oscillateur à quartz mesuré, la prédiction mise de côté est prudente mais n'atteint pas le seuil, de sorte que le cas du quartz est MODELLED. (catalogue des types (kshana kinds --json))
• MODELLED : les sources de classe et de fiche technique, les termes déterministes et l'évaluation du leurrage. (catalogue des types (kshana kinds --json))

Voir aussi#

• Page de famille : Horloges, synchronisation temporelle et holdover
• Tous les types de scénario : KINDS.md
• Page thématique : LEO-PNT.md
• Page thématique : DECEIVED-TIME.md