Машинний переклад, не перевірений носієм мови. Еталоном є англійська версія.

Сторінки видів сценаріївРедагувати на GitHubДжерело: docs/kinds/by-kind/integrity.md

integrity (вид сценарію)

Різновид сценарію рушія v0.40.0, родина Вимірювання GNSS, позиціонування та цілісність. Лише консультативно: результат аналізу від дослідницького та інженерного інструмента; це не навігаційне обладнання із затвердженням типу і не послуга забезпечення безпеки життя. Кожна позначка тут — рушія або матриці верифікації; різновид є MODELLED, якщо матриця не каже іншого (як заслужити позначку: розділ README про докази).

Що він робить#

RAIM миттєвий / із розділенням розв'язків / ARAIM з HPL/VPL і діаграмою Стенфорда.

Один прогін scenarios/integrity-raim.toml підсумовується так: integrity | 24 satellites | 344/361 epochs available (95,3%) | HAL 40 m VAL 50 m | sigma 1,0 m | Stanford(V): 0 integrity events, 0 HMI

Входи#

Зі схеми (kshana kinds --json):

  • Обов'язкові поля: mask_deg, sigma_uere_m, p_fa, p_md, al_h_m, al_v_m, time, user|user_site, constellation
  • Необов'язкові поля: sigma_ura_m, b_nom_m, constellations, seed, araim_dual, p_hmi, skyline

Приклад scenarios/integrity-raim.toml задає, зокрема:

Поле Значення Одиниця
al_h_m 40 m
al_v_m 50 m
constellation.altitude_km 20200 km
constellation.inclination_deg 55 deg
constellation.phasing_f 1 не вказано
constellation.planes 6 не вказано
constellation.sats_per_plane 4 не вказано
kind integrity text
mask_deg 5 deg
p_fa 1.0000e-5 не вказано
p_md 0.001 не вказано
seed 7 не вказано

Запуск#

kshana scenarios/integrity-raim.toml

Цей тип використовують 3 вбудовані сценарії; решта — у scenarios/.

Що це дає#

Скалярні результати цього прогону з одиницями, які вказує рушій:

Результат Значення Одиниця
al_h_m 40 m
al_v_m 50 m
evidence.id_rule стабільний ідентифікатор рядка матриці (ID text
evidence.matrix docs/VERIFICATION-MATRIX.md text
evidence.tier MODELLED text
samples_available 344 кількість
samples_total 361 кількість
stanford.alert_limit_m 50 m
Діаграма, яку рушій записує для scenarios/integrity-raim.toml, вид integrity

Докази#

MODELLED 6 · VALIDATED 4: рядки матриці верифікації, що згадують цей вид.

  • MODELLED Необов'язковий розділ [integrity] типу clock (clock_integrity::run): із заявленого майданчика та пресетів орбітальних угруповань (geometry::sky_geometry), на кожну епоху цілісності, поки часова шкала GNSS не заперечена, знімок RAIM (raim::snapshot_ Тести: clock_integrity.rs.
  • VALIDATED TPL із розділенням розв'язків за скалярним часом для різнорідних джерел; PL визначається шумом підмножини з найгіршим виключенням + зміщенням UTC(k)
  • MODELLED PL(τ)=max(TPL_handover,HPL(τ)); нижньонапівнеперервний PL(0+)≥PL(0−); K(IR/2) рухомий максимум; фазові показники степеня τ/τ³/τ⁵
  • VALIDATED Огинна рухомого максимуму перекриває з запасом (без проколів) реальний метрологічний ряд за кожного перевіреного зсуву tau>=90d на непересічному сегменті; коротке tau (<=30d) — це оголошена межа рівня Modelled Тести: cti_holdover_coverage_reference.rs.
  • і ще 6 у матриці.

Рядки, які задіяв сам прогін, з оракулом, що його дає матриця кожному (публічні джерела названі там):

  • VALIDATED Розв'язок ARAIM із розділенням рішень за багатьма гіпотезами згідно з ARAIM Airborne Design Document (ADD) v4.2 (araim_reference::add_v42_protection_levels і add_v42_protecti. Оракул (ExternalDataset): Три незалежні інструменти, попередньо зареєстровані (0123cee1) до появи будь-яких фікстур чи виходів оракула, допуски зафіксовано тоді. (1) ARAIM: Stanford MAAST для ARAIM 2 (коміт ab70e2a3, BSD-3) mhss_raim_baseline_v5.m, запущений як окрема програма під GNU Octave 8,4 зі сумісним шимом unique() на боці драйвера (розкрито, без зміни алгоритму), за ADD TOL_PL 0,05 м: Rust відтворює еталонну реалізацію ADD на
  • VALIDATED GDOP/PDOP/HDOP/VDOP/TDOP із геометрії ліній візування через Q=(HᵀH)⁻¹ з локальним розкладом ENU. Оракул (ExternalDataset): gnss_lib_py 1.0.4 (Stanford NAV Lab) DOP — незалежна бібліотека, збіг до 1e-6 відносної похибки
  • VALIDATED Розподільне ядро, на якому тримається кожен рівень захисту: поріг виявлення відмов за знімком χ²₁₋ₚfₐ(dof), нецентральність пропущеного виявлення pbias=√λ та . Оракул (ExternalDataset): SciPy 1.17.0 (scipy.stats.chi2/.norm/.ncx2 + optimize.brentq) — незалежна бібліотека (Cephes/Boost), інший алгоритм, ніж ряд неповної гамма-функції в Kshana; збіг до ≤1e-6 відн. Лише ядро. Розподіл бюджету P_HMI для ARAIM MHSS більше не залишається без опублікованого числового оракула — власний робочий приклад Технічної підгрупи ARAIM WG-C тепер підтримує окремий рядок «ARAIM MHSS protection levels against published referen
  • MODELLED Детерміновані, хешовані за сценарієм, SBOM + міжплатформні еталонні шлюзи. Оракул (ExternalDataset): відповідність SBOM офіційній схемі JSON CycloneDX 1,5 (+ дійсні ідентифікатори SPDX) — зовнішній опублікований стандарт, нуль помилок валідації на всьому графі залежностей; частина щодо детермінованості FoM / побайтової відтворюваності залишається закріпленою перевіркою самоузгодженості, тому рядок залишається MODELLED

Обмеження#

Що, за власним звітом прогону, не обчислено за моделлю або не перевірено за зовнішнім еталоном:

  • Відтворюваність і гарантування якості програмного забезпечення — MODELLED, а не перевірено за зовнішнім еталоном: підтвердження частини вимоги перевірено зовні, але вся можливість складається з обчислених за моделлю частин, тому можливість залишається обчисленою за моделлю. (матриця верифікації (docs/MODELLED-RATIONALE.md))

Див. також#