Tradução automática, não revista por um falante nativo. O inglês é a referência.

Páginas de tipos de cenárioEditar no GitHubFonte: docs/kinds/by-kind/clock.md

clock (tipo de cenário)

Tipo de cenário do motor v0.40.0, família Relógios, temporização e holdover. Consultivo: saída de análise de uma ferramenta de pesquisa e engenharia, não um equipamento de navegação homologado e não um serviço de segurança da vida humana. Todo rótulo aqui é do motor ou da matriz de verificação; um tipo de cenário é MODELLED, a menos que a matriz diga outra coisa (como um rótulo é conquistado: a seção Evidence do README).

O que faz#

Holdover do relógio em relação à especificação; conjunto Monte Carlo opcional (execuções > 1).

Uma execução de scenarios/clock-ensemble.toml resume-se assim: cenário 91d2b6d10d14 | 200 execuções | holdover quântico 6600s [6600-6600] p95 8.78e-4ns segurança n/d (sem ataque) | holdover clássico 844s [220-2130] p95 167.0ns segurança n/d (sem ataque)

Entradas#

A partir do esquema (kshana kinds --json):

  • Campos obrigatórios: seed, threshold_ns, time, gnss, clock_quantum, clock_classical
  • Campos opcionais: runs, integrity

O exemplo scenarios/clock-ensemble.toml define, entre outros:

Campo Valor Unidade
clock_classical.flicker_floor 2.0000e-11 1
clock_classical.id csac-sa45s texto
clock_classical.provenance Folha de dados do CSAC Microchip SA65 / SA.45s 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 Relógio óptico de rede de estrôncio, meta para uso espacial 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

Execute#

kshana scenarios/clock-ensemble.toml

6 cenários incluídos usam este tipo; os demais estão em scenarios/.

O que ele fornece#

Os resultados escalares dessa execução, com as unidades que o motor declara:

Resultado Valor Unidade
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
O gráfico que o motor gera para scenarios/clock-ensemble.toml, tipo de cenário clock

Evidências#

MODELLED: as linhas da matriz de verificação que nomeiam este tipo de cenário.

  • MODELLED A seção opcional [integrity] do tipo de cenário clock (clock_integrity::run): a partir de um local e de predefinições de constelação declarados (geometry::sky_geometry), em cada época de integridade enquanto a linha do tempo do GNSS não está negada, RAIM instantâneo (raim::snapshot_ Testes: clock_integrity.rs.
  • MODELLED clock_log::read_input: uma camada de análise sintática que converte um arquivo de relógio RINEX (registros AS/AR de um relógio nomeado, versões 2 e 3,00 a 3,04), um registro ASCII de fase ou frequência no estilo TimeLab, ou um registro de carimbos de tempo ou intervalos do TAPR TICC em um pha uniforme Testes: clock_log_allantools.rs.
  • MODELLED clock_log::read_input com os formatos ptp4l, phc2sys, ts2phc, chrony-tracking e chrony-statistics: o desvio registrado de uma linha de servo do linuxptp (ns, o carimbo de tempo entre colchetes da própria linha, leituras antes de o servo informar s2 pela primeira vez omitidas a
  • MODELLED O tipo de cenário mission-thread: um documento de fases, cada uma de um de oito tipos registrados, executadas em ordem com a covariância 6x6, o relógio e o referencial transferidos sob uma regra declarada (carry; inflate, ruído de aceleração branco ao longo de um intervalo declarado Testes: field_units_global.rs.
  • e mais 1 na matriz.

As linhas que a própria execução exercitou, com a referência independente que a matriz dá a cada uma (as fontes públicas são nomeadas ali):

  • VALIDATED Desvio de Allan/modificado/Hadamard + identificação de ruído de lei de potência com ICs de χ². Referência independente (ExternalDataset): NIST SP 1065 (Riley) / desvios de referência do Stable32 em NBS14
  • MODELLED Crescimento do erro em inércia de forma fechada + holdover até o limiar; classes de relógios quânticos. Referência independente (ReferenceImpl): Recursão de covariância multipasso de clock_state (conferência cruzada na mesma base de código); o núcleo subjacente de variância de deriva e inversão de holdover é validado externamente contra o scipy (ver 'Clock-holdover coast-variance & threshold inversion'). Os valores de holdover por classe com piso de ruído vermelho permanecem MODELLED
  • MODELLED Relógio de Kalman de 3 estados (fase/frequência/deriva) de van Loan, estabilizado por Joseph. Referência independente (ReferenceImpl): KalmanFilter do filterpy 1.4.5 (R. Labbe, MIT), com F via scipy.linalg.expm e Q via a matriz em blocos de Van Loan 1978 — uma implementação de referência independente que reproduz a trajetória completa do filtro do kshana. Consistência entre implementações: a física do relógio / a calibração de Allan não são validadas externamente, por isso isto permanece MODELLED. Comparação externa 0,30, um achado (permanece MODELLED): em relógios finais do IGS de 30 s de 11 GPS Blo
  • MODELLED χ² auxiliado pelo relógio, RAIM, AGC e SQM fundidos em uma figura de mérito de segurança por época. Referência independente (ExternalDataset): parâmetros de cenário do TEXBAT (Humphreys 2012) — caracterização, não vetores fixados. Comparação externa 0,30, um achado (permanece MODELLED): no JammerTest 2024 (Bleik; dados GPL-3.0) os monitores em nível de observável (qui-quadrado auxiliado pelo relógio, RAIM, falha de solução) não levantaram alarme em até 10 s de nenhum dos 8 inícios de spoofing publicados avaliáveis (onde a janela anterior ao início estava limpa, o primeiro alarme veio de 10,2 a 39 s após o pu
  • MODELLED Portões determinísticos, com hash de cenário, de SBOM e de golden entre plataformas. Referência independente (ExternalDataset): aderência à norma do SBOM ao JSON Schema oficial do CycloneDX 1,5 (+ identificadores SPDX válidos) — um padrão externo publicado, zero erros de validação em todo o grafo de dependências; a parte de determinismo das FoMs / reprodutibilidade byte a byte continua sendo uma verificação de autoconsistência fixada, de modo que a linha permanece MODELLED

Limitações#

O que o próprio relatório da execução diz que não é modelado ou não é validado:

  • O holdover do relógio sem GNSS é MODELLED, não validado: conferido contra uma implementação separada nesta mesma base de código — independente da unidade sob teste, mas sem autoridade externa. (matriz de verificação (docs/MODELLED-RATIONALE.md))
  • A estimativa do estado do relógio a bordo é MODELLED, não validada: conferida contra uma implementação separada nesta mesma base de código — independente da unidade sob teste, mas sem autoridade externa. (matriz de verificação (docs/MODELLED-RATIONALE.md))
  • A detecção de spoofing é MODELLED, não validada: uma subafirmação é conferida externamente, mas a capacidade inteira compõe peças modeladas, de modo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))
  • Reprodutibilidade e garantia de software é MODELLED, não validada: uma subafirmação é verificada externamente, mas a capacidade inteira compõe peças modeladas, de modo que a capacidade permanece modelada. (matriz de verificação (docs/MODELLED-RATIONALE.md))

Veja também#