mars-pnt (вид сценарію)
Тип сценарію рушія v0.40.0, родина Орбітальні угруповання, покриття та геометрія. Лише консультативно: результат аналізу від дослідницького та інженерного інструмента; це не навігаційне обладнання із затвердженням типу і не послуга забезпечення безпеки життя. Кожна позначка тут належить рушієві або матриці верифікації; тип вважається MODELLED, якщо матриця не каже іншого (як заробляється позначка: розділ Evidence у README).
Що він робить#
PNT у далекому космосі на Марсі: симульоване орбітальне угруповання ретрансляторів MARCONI (ареостаціонарні та похилі ретранслятори, що передають в один бік + ретранслюють у два боки до станції далекого космосу) навігує опорного користувача (transfer | lmo | surface) через спільний оцінювач злиття радіометричних вимірювань в один і два боки. Звітує про геометрію/видимість для кожної епохи, досягнуту СКВ відносно істини та формальну коваріацію (1σ / 3σ положення) — чесний симульований показник якості, а НЕ сертифікований рівень захисту.
Один прогін scenarios/mars-pnt-lmo.toml підсумовується так: mars-pnt 5aad87fcc94a | користувач lmo, годинник uso | 5 ретрансляторів (у середньому 3,1 у полі зору) | збіжна СКВ положення 0,25 м, формальне 1σ 0,31 м (3σ 0,93 м — показник якості за коваріацією, а не сертифікований PL) | σ частоти годинника 3.71e-13 | cov-PD true
Входи#
Зі схеми (kshana kinds --json):
- Обов'язкові поля: немає
- Необов'язкові поля:
user,clock_class,step_s,duration_s,nmax,range_sigma_m,doppler_sigma_mps,dynamic_tightness,two_way_period_s,seed
Приклад scenarios/mars-pnt-lmo.toml задає, зокрема:
| Поле | Значення | Одиниця |
|---|---|---|
clock_class |
uso | text |
doppler_sigma_mps |
1.0000e-4 | m/s |
duration_s |
7200 | s |
dynamic_tightness |
0.1 | не вказано |
kind |
mars-pnt | text |
nmax |
4 | не вказано |
range_sigma_m |
1 | m |
seed |
331514052 | не вказано |
step_s |
60 | s |
two_way_period_s |
1800 | s |
user |
lmo | text |
Запуск#
kshana scenarios/mars-pnt-lmo.toml
Цей тип використовують 3 вбудовані сценарії; решта — у scenarios/.
Що це дає#
Скалярні результати цього прогону з одиницями, які вказує рушій:
| Результат | Значення | Одиниця |
|---|---|---|
areostationary_radius_m |
2.0428e7 | m |
clock_class |
uso | text |
evidence.id_rule |
стабільний ідентифікатор рядка матриці (ID | text |
evidence.matrix |
docs/VERIFICATION-MATRIX.md | text |
evidence.tier |
MODELLED | text |
fom.converged_pos_3sigma_m |
0.927387 | m |
fom.converged_pos_rms_m |
0.245604 | m |
fom.converged_pos_sigma_m |
0.309129 | m |
fom.covariance_pd_throughout |
true | flag |
fom.epochs |
120 | кількість |
Докази#
MODELLED: рядки матриці верифікації, що називають цей різновид.
- MODELLED Тип
body-pnt: орбітальний апарат або посадковий модуль на поверхні навколо тіла, обраного за назвою, навігується за односторонніми псевдодальностями від навігаційного орбітального угруповання Волкера навколо тіла (двотільні орбіти з вековим дрейфом J2 тіла, невідомий годинник користувача
Рядки, які задіяв сам прогін, з оракулом, що його дає матриця кожному (публічні джерела названі там):
- VALIDATED Відновлення стану епохи [r,v] за відстанями від наземних станцій пакетним диференційним коректором Гаусса–Ньютона та послідовним фільтром на силовій моделі двох тіл+J2. Оракул (ExternalDataset): Orekit 12,2 (CS GROUP, Apache-2.0) BatchLSEstimator (Левенберга–Марквардта) + KalmanEstimator (EKF) — незалежна стороння бібліотека оцінювання на узгодженій силовій моделі; відновлений стан епохи + післяпідгоночна СКВ нев'язки збігаються до <1e-3 м без шуму та <3 м за рівня шуму 5 м
- MODELLED 3-становий (фаза/частота/дрейф) годинник Калмана van-Loan зі стабілізацією за Джозефом. Оракул (ReferenceImpl): filterpy 1.4.5 KalmanFilter (R. Labbe, MIT), з F через scipy.linalg.expm та Q через блокову матрицю Van-Loan 1978 — незалежна еталонна реалізація, що відтворює повну траєкторію фільтра kshana. Узгодженість між реалізаціями: фізика годинника / калібрування Аллана не перевірені зовнішньо, тому це лишається MODELLED. 0,30 зовнішнє порівняння, знахідка (лишається MODELLED): на фінальних годинниках IGS 30 с для 11 блоків GPS
- MODELLED Детерміновані, хешовані за сценарієм, SBOM + міжплатформні еталонні шлюзи. Оракул (ExternalDataset): відповідність SBOM офіційній схемі JSON CycloneDX 1,5 (+ дійсні ідентифікатори SPDX) — зовнішній опублікований стандарт, нуль помилок валідації на всьому графі залежностей; частина щодо детермінованості FoM / побайтової відтворюваності залишається закріпленою перевіркою самоузгодженості, тому рядок залишається MODELLED
Обмеження#
Що, за власним звітом прогону, не обчислено за моделлю або не перевірено за зовнішнім еталоном:
- Оцінювання стану бортового годинника є MODELLED, а не перевіреним (validated): звірено з окремою реалізацією в цій самій кодовій базі — незалежною від тестованого модуля, але не зовнішньо авторитетною. (матриця верифікації (docs/MODELLED-RATIONALE.md))
- Відтворюваність і гарантування якості програмного забезпечення — MODELLED, а не перевірено за зовнішнім еталоном: підтвердження частини вимоги перевірено зовні, але вся можливість складається з обчислених за моделлю частин, тому можливість залишається обчисленою за моделлю. (матриця верифікації (docs/MODELLED-RATIONALE.md))
Див. також#
- Сторінка родини: Орбітальні угруповання, покриття та геометрія
- Усі різновиди: KINDS.md
- Тематична сторінка: SOLAR-SYSTEM.md