Traducción automática, no revisada por un hablante nativo. El inglés es la referencia.

Páginas de tipos de escenarioEditar en GitHubFuente: docs/kinds/by-kind/clock.md

clock (tipo de escenario)

Tipo de escenario del motor v0.40.0, familia Relojes, temporización y holdover. Consultivo: salida de análisis de una herramienta de investigación e ingeniería, no un equipo de navegación homologado ni un servicio de seguridad de la vida humana. Toda etiqueta de aquí es la del motor o la de la matriz de verificación; un tipo de escenario es MODELLED salvo que la matriz diga otra cosa (cómo se gana una etiqueta: la sección Evidence del README).

Qué hace#

Holdover del reloj frente a la especificación; conjunto de Monte Carlo opcional (ejecuciones > 1).

Una ejecución de scenarios/clock-ensemble.toml se resume así: 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)

Entradas#

Del esquema (kshana kinds --json):

  • Campos obligatorios: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Campos opcionales: runs, integrity

El ejemplo scenarios/clock-ensemble.toml establece, entre otros:

Campo Valor Unidad
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s texto
clock_classical.provenance Microchip SA65 / SA.45s CSAC datasheet sigma_y(1s)=3e-10; q_ texto
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 texto
clock_quantum.provenance Reloj óptico de red de estroncio, objetivo orientado al espacio sigma_y texto
clock_quantum.q_rw 0 1/s
clock_quantum.q_wf 1.0000e-30 s^2/s
clock_quantum.y0 5.0000e-17 1

Ejecútelo#

kshana scenarios/clock-ensemble.toml

6 escenarios incluidos usan este tipo de escenario; los demás están en scenarios/.

Qué proporciona#

Los resultados escalares de esa ejecución, con las unidades que indica el motor:

Resultado Valor Unidad
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 indicador
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
El gráfico que escribe el motor para scenarios/clock-ensemble.toml, tipo de escenario clock

Evidencias#

MODELLED: las filas de la matriz de verificación que nombran este tipo de escenario.

  • MODELLED La sección opcional [integrity] del tipo de escenario clock (clock_integrity::run): a partir de un emplazamiento indicado y de preajustes de constelación (geometry::sky_geometry), en cada época de integridad mientras la línea temporal GNSS no está denegada, RAIM instantáneo (raim::snapshot_ Pruebas: clock_integrity.rs.
  • MODELLED clock_log::read_input: una capa de análisis sintáctico que convierte un archivo de reloj RINEX (registros AS/AR de un reloj con nombre, versiones 2 y 3,00 a 3,04), un registro ASCII de fase o de frecuencia de estilo TimeLab, o un registro de marcas de tiempo o de intervalos de TAPR TICC en una fase uniforme Pruebas: clock_log_allantools.rs.
  • MODELLED clock_log::read_input con los formatos ptp4l, phc2sys, ts2phc, chrony-tracking y chrony-statistics: el desfase registrado de una línea del servo de linuxptp (ns, la propia marca de tiempo entre corchetes de la línea, con las lecturas anteriores a la primera vez que el servo informa de s2 omitidas a
  • MODELLED El tipo de escenario mission-thread: un documento de fases, cada una de uno de ocho tipos registrados, ejecutadas en orden con la covarianza de 6x6, el reloj y el marco transmitidos bajo una regla indicada (carry; inflate, ruido de aceleración blanco sobre un intervalo indicado Pruebas: field_units_global.rs.
  • y 1 más en la matriz.

Las filas que la propia ejecución puso a prueba, con la referencia independiente que da la matriz a cada una (las fuentes públicas se nombran allí):

  • VALIDATED Desviación de Allan / modificada / de Hadamard + identificación de ruido de ley de potencias con intervalos de confianza χ². Referencia independiente (ExternalDataset): NIST SP 1065 (Riley) / desviaciones de referencia de Stable32 en NBS14
  • MODELLED Crecimiento del error de inercia en forma cerrada + holdover hasta el umbral; clases de reloj cuántico. Referencia independiente (ReferenceImpl): Recursión de covarianza de clock_state en varios pasos (comprobación cruzada en el mismo código base); el núcleo subyacente de varianza de inercia e inversión de holdover está validado externamente frente a scipy (véase «Clock-holdover coast-variance & threshold inversion»). Las cifras de holdover por clase con suelo de ruido rojo siguen siendo MODELLED
  • MODELLED Reloj de Kalman de 3 estados (fase/frecuencia/deriva) de van Loan, estabilizado de Joseph. Referencia independiente (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), con F mediante scipy.linalg.expm y Q mediante la matriz por bloques de Van Loan 1978 — una implementación de referencia independiente que reproduce la trayectoria completa del filtro de kshana. Consistencia entre implementaciones: la física del reloj y la calibración de Allan no están validadas externamente, por lo que esto sigue siendo MODELLED. 0,30 comparación externa, un hallazgo (sigue siendo MODELLED): en relojes finales de IGS de 30 s de 11 GPS Blo
  • MODELLED Chi-cuadrado asistido por reloj, RAIM, AGC, FoM de seguridad por época fusionada con SQM. Referencia independiente (ExternalDataset): parámetros de escenario de TEXBAT (Humphreys 2012) — caracterización, no vectores fijados. 0,30 comparación externa, un hallazgo (sigue siendo MODELLED): en JammerTest 2024 (Bleik; datos GPL-3.0) los monitores de nivel de observable (chi-cuadrado asistido por reloj, RAIM, fallo de solución) no dieron ninguna alarma dentro de 10 s de ninguno de los 8 inicios de suplantación publicados evaluables (donde la ventana previa al inicio estaba limpia, la primera alarma llegó entre 10,2 y 39 s después del pu
  • MODELLED Determinista, con hash de escenario, SBOM + barreras golden multiplataforma. Referencia independiente (ExternalDataset): ajuste a la norma del SBOM al esquema JSON oficial de CycloneDX 1,5 (+ identificadores SPDX válidos) — un estándar externo publicado, cero errores de validación en todo el grafo de dependencias; la parte de determinismo de FoM / reproducibilidad byte a byte sigue siendo una comprobación de autoconsistencia fijada, por lo que la fila sigue siendo MODELLED

Limitaciones#

Lo que el propio informe de la ejecución dice que no está modelado o no está validado:

  • El holdover del reloj sin GNSS es MODELLED, no está validado: se comprueba frente a una implementación separada de este mismo código base — independiente de la unidad bajo prueba, pero no autoridad externa. (matriz de verificación (docs/MODELLED-RATIONALE.md))
  • La estimación del estado del reloj de a bordo es MODELLED, no está validada: se comprueba frente a una implementación separada de este mismo código base — independiente de la unidad bajo prueba, pero no autoridad externa. (matriz de verificación (docs/MODELLED-RATIONALE.md))
  • La detección de spoofing es MODELLED, no está validada: una subafirmación se comprueba externamente, pero la capacidad completa compone piezas modeladas, por lo que la capacidad sigue siendo modelada. (matriz de verificación (docs/MODELLED-RATIONALE.md))
  • La reproducibilidad y el aseguramiento del software son MODELLED, no están validados: una subafirmación se comprueba externamente, pero la capacidad completa compone piezas modeladas, por lo que la capacidad sigue siendo modelada. (matriz de verificación (docs/MODELLED-RATIONALE.md))

Véase también#