Executive Summary
This bundle collects the verification evidence for the MetaSpace.bio Fault Detection, Isolation, and Recovery (FDIR) detector and separates what is formally proved, what is measured in simulation and what is only assumed. It is not a certification: no assessment by an accredited body has taken place. The work targets IEC 61508 SIL 3.
Status: SIMULATION-VALIDATED · SIL 3 TARGETED · NOT CERTIFIED (TRL 3-4, software only; no flight hardware).
Evidence Dashboard
Status of each audit gap, with the strength of its evidence (PROVED, MEASURED in simulation, or ASSUMED). Reproduce with the commands in the Claims Ledger.
| Gap ID | Requirement | Status | Evidence | Source Data |
|---|---|---|---|---|
| GAP-0 | Detector logic conforms to the .bio specification | PROVED | 15 Z3 proofs (IEEE-754 float64, all inputs incl. NaN/inf), 1565-vector differential test, 8 mutation controls | Transcript |
| GAP-1.1 | Numerical verification (reference RK4 routine; simulator time-step refinement) | MEASURED | RK4 reference order 4.01 / 4.00 (checks the method; the simulator does not use RK4). Simulator battery deviation falls from 1.71 to 0.23 percentage points as the step goes from 2.0 to 0.25 min (first order) | JSON |
| GAP-2.1 | Model self-consistency vs closed-form energy balance | MEASURED | MAE 0.0000 percentage points, correlation 1.000000; 3 of 3 perturbed references rejected (same equations; not real telemetry) | JSON |
| GAP-3.1 | PFD arithmetic (illustrative) | ASSUMED | Placeholder inputs; 2e-06 to 5e-04 depending on the assumed DC and beta; no SIL claimed | JSON |
| GAP-4.1 | FDIR detection in simulation | MEASURED | 135-case guard sweep: 0 missed, 0 false alarms. Injected faults reach the detector in the first cycle (smoke test, by construction). 200000 nominal cycles without false alarm (consistency check). TC-GPS-01, TC-SOLAR-01 and TC-BATT-01 are executable tests. No hardware | JSON |
01 Safety Case: MetaSpace FDIR System (Draft)
Date: 2026-10-31
Status: DRAFT - simulation-validated, SIL 3 targeted, NOT CERTIFIED
1. Executive Summary
This draft safety case targets IEC 61508 SIL 3. No assessment by an accredited body has taken place. The detector logic is formally proved against its specification (see the Formal Verification section). The quantitative figure below is illustrative arithmetic on assumed placeholder inputs and supports no SIL claim.
2. Illustrative PFD arithmetic
Simplified low-demand 1oo2 form (design target, not implemented here), PFD = (λDUT)2/3 + βλDUT/2 with λDU = λtotal(1 - DC). All inputs are ASSUMED:
| Parameter | Value | Source |
|---|---|---|
| Architecture | 1oo2 (Redundant) - design target, not implemented | Design intent |
| Total failure rate | 850 FIT | Placeholder rates of the monitored units (GPS, IMU, CPU, power bus) |
| Diagnostic Coverage (DC) | 99% (nominal point; varied 60-99%) | Assumed target |
| Proof Test Interval | 3 Years | Assumed |
| PFD avg at the nominal point | 5.60e-06 | Arithmetic on assumed inputs |
| PFD avg over DC 0.60-0.99 and β 0.02-0.10 | 2.3e-06 to 4.7e-04 | Sensitivity grid |
3. Statement
With the same placeholder inputs the result falls in the following IEC 61508 low-demand bands depending on the assumed coverage and beta: SIL 3 band, SIL 4 band, below the SIL 4 band (<1e-5). The figure therefore supports no SIL claim.
CONCLUSION: SIL 3 is a design target. Measured failure data for the FDIR function, an implemented redundant architecture and an independent assessment are still required. This is not a compliance or certification claim.
03 Detailed Validation Report
Date: 2026-10-31
1. Numerical verification
Audit Gap 1.1. Two separate checks. (A) A reference RK4 routine reaches its theoretical order on a damped oscillator with a known exact solution: observed orders 4.0087 and 4.0045 (theoretical 4). This checks the method, not the simulator. (B) The simulator's own integration is an explicit Euler update (RK4 is not used by the simulator). Refining its time step from 2.0 to 0.25 min reduces the maximum battery state-of-charge deviation from the finest run (0.05 min) from 1.71 to 0.23 percentage points, i.e. first-order behaviour dominated by where the eclipse boundary falls inside a step.
2. Model self-consistency
Audit Gap 2.1. The simulated energy balance was compared with a closed-form re-implementation of the same documented model. This checks the implementation against its own specification; it is not validation against real telemetry. Three deliberately perturbed references (load +10%, generation -50%, eclipse 50%) were rejected: 3 of 3.
| Metric | Result | Criterion | Status |
|---|---|---|---|
| Correlation | 1.000000 | > 0.9999 | PASS |
| Mean Absolute Error (MAE) | 0.000000 percentage points | < 0.01 | PASS |
3. FDIR fault injection (smoke test and sweep)
Audit Gap 4.1. Injected faults reach the detector in the first cycle of the simulation (assumed 10 ms cycle). This is a smoke test: the fault is applied to the detector input in the same pass that evaluates it, so first-cycle detection holds by construction and is not a latency measurement.
Separately, the detector was swept over 135 guard-level cases (missed detections: 0, false alarms: 0) and 200000 nominal-noise cycles (false alarms: 0; a consistency check, the margin is at least 10 sigma).
The test cases TC-GPS-01, TC-SOLAR-01 and TC-BATT-01 are executable in backend/tests/test_fdir_cases.py.
| Scenario | Cycles to detect (x assumed 10 ms) | Detection Rate |
|---|---|---|
| GPS Spoofing | 1 cycle(s) = 10.00 ms simulated | 100.0% |
| Solar Panel Failure | 1 cycle(s) = 10.00 ms simulated | 100.0% |
| Battery Failure | 1 cycle(s) = 10.00 ms simulated | 100.0% |
4. Final Verdict
The checks above were executed and reproduce from the repository. They are simulation-level evidence and do not constitute certification. See CLAIMS_LEDGER.md for the proved / measured / assumed classification of every claim.
Supporting Documentation
The following technical documents provide the detailed derivation and analysis supporting the certification.
System Architecture: 1oo2 Redundancy
System: MetaSpace.bio FDIR Configuration: 1oo2 (One-out-of-Two) Safety Logic Status: DESIGN TARGET. Only a single detector channel (`fdir_guard`) is implemented in this repository; the redundant second channel, voting and diversity measures below are not implemented or tested.
---
1. Architecture Overview
The MetaSpace.bio system utilizes a 1oo2 (One-out-of-Two) architecture to maximize safety and fault detection probability. In this configuration, two independent FDIR channels operate in parallel. If either channel detects a violation of the physical invariants (Bio-Codes), the system triggers the fail-safe recovery mode ("Safe Mode").
This architecture is chosen to prioritize Safety (SIL 3 targeted) over Availability, aiming to minimize the Missed Detection Rate.
---
2. Block Diagram
SENSORS: GPS Receiver, IMU / Gyro, Power System
| |
+------+------+ +------+------+
| FDIR Channel A | | FDIR Channel B | (Processing Core, dual channel)
+------+------+ +------+------+
| Fault Signal A | Fault Signal B
+----------+----------+
|
[1oo2 VOTER] IF A OR B
|
[Safe Mode Trigger]
|
[Recovery Sequencer] (Actuators)---
3. Operational Logic
1oo2 Voting Rule
The voter implements a logical OR function for fault declaration:Channel Independence
---
4. Failure Modes and Effects
| Event | Description | System Response | Safety Impact |
|---|---|---|---|
| Channel A Failure | Channel A stops functioning or crashes. | Channel B continues monitoring. System remains safe (1oo1 fallback). | Minimal (Redundancy lost) |
| Channel A False Alarm | Channel A detects fault when none exists. | Voter triggers Safe Mode (False Positive). | Availability reduced, Safety maintained. |
| Real Fault (e.g. GPS Spoofing) | Both channels detect violation. | Safe Mode Triggered. | SAFE (Hazard mitigated). |
| Channel A Missed Detection | Channel A fails to see fault. Channel B detects it. | Safe Mode Triggered. | SAFE (1oo2 benefit). |
| Common Cause Failure | Both channels fail simultaneously (e.g. EMP, Power loss). | Watchdog Timer (Hardware) resets system. | Critical (Mitigated by Watchdog). |
---
5. Conclusion
The 1oo2 architecture is intended to raise system-level detection probability by allowing either of two independent monitors to arrest a dangerous situation. A diagnostic coverage of >99% is a target, not an achieved or measured value. The assumed-input PFD estimate is in `SIL3_PFD_Calculation.md`.
Diagnostic Coverage (DC) Analysis
System: MetaSpace.bio FDIR Status: analysis of intended coverage with ASSUMED figures. DC is a target (> 99.0%), not a measured or certified value.
---
1. Methodology
Diagnostic Coverage (DC) is defined as the ratio of the failure rate of detected dangerous failures to the failure rate of all dangerous failures:
DC = lambda_DD / lambda_Dtotal
The detector (`fdir_guard.detect`) applies one threshold to one residual per channel: it is a range check on a residual, formally proved against its specification. Computing the residual from physics (position against propagated position, power balance, attitude against star tracker, torque against angular acceleration) is the job of the surrounding system. In this repository the simulator passes its `gps_error` and `imu_accumulated_error` values in as the residuals; the power, wheel and battery residuals are not generated.
---
2. Failure Mode Coverage Matrix
| Fault ID | Failure Mode | Detectable by Physics? | Invariant Violated | Evidence level |
|---|---|---|---|---|
| FM-01 | GPS Spoofing | YES | Spatial Invariant: satellite cannot teleport or accelerate faster than F/m. | Proved (detector logic, all float64 inputs) + simulated injection |
| FM-02 | Solar Panel Loss | YES | Energy Invariant (intended): Power In ≠ Power Stored + Consumed. As implemented in the simulator: battery level below 20 % / 40 % or generation at or below 1200 W (threshold rules, not an energy-balance residual). | Detector channel proved; the simulator detects it through its battery/solar-output rule, which is not covered by the proof |
| FM-03 | Battery Short | YES | Energy Invariant: sudden voltage drop without load change. | Detector channel proved; not fed by the simulator; threshold illustrative |
| FM-04 | IMU Drift | YES | Temporal Invariant: integrated rate does not match star-tracker vector. | Proved (detector logic) + simulated injection |
| FM-05 | Reaction Wheel Stick | YES | Momentum Invariant: torque applied ≠ angular acceleration observed. | Detector channel proved; not fed by the simulator; threshold illustrative |
| FM-06 | CPU Bitflip (SEU) | PARTIAL | Memory checksums + logic-flow check. | Not implemented or tested here |
"Proved" means: the detector function conforms to the specification. It does not mean the physical failure is detected with a given probability, which depends on real sensor behaviour and threshold calibration.
---
3. Aggregate DC
The coverage numbers used in earlier revisions of this document (e.g. "> 99.5%", "> 98%", "0.9784 weighted") were estimates without measurement. They are withdrawn. The PFD arithmetic uses DC only as an assumed input and reports how its result changes with it (see PFD Arithmetic).
A defensible DC figure requires a fault-injection campaign on representative hardware with real sensor data and a classified FMEA. This has not been done.
---
4. Verification evidence available today
1. `verify_guard_conformance.py` — Z3 proof that the detector guard conforms to `satellite_fdir.bio` (every channel breach is detected; no breach gives no fault; NaN inputs fail safe), with differential testing and mutation controls. 2. `measure_fdir_detection.py` — 135-case channel sweep: 0 missed detections, 0 false alarms; simulator injection of GPS and IMU faults detected in the same cycle. 3. `fdir_performance_metrics.py` — three injected scenarios reach the detector in the first cycle. This is a smoke test: the fault is applied to the detector input in the same pass that evaluates it, so first-cycle detection holds by construction. 4. `backend/tests/test_fdir_cases.py` — executable TC-GPS-01, TC-SOLAR-01 and TC-BATT-01 with negative controls; for solar and battery the detector inputs come from the model telemetry after a real failure injection.
FDIR Performance Metrics: TTD, FAR, MDR
Status: simulation measurements. Not hardware, not real-time, not certified. See `CLAIMS_LEDGER.md`. Data sources: `results/fdir_performance_report.json` (3 smoke-test scenarios, 100 seeded runs each) and `results/fdir_measured_report.json` (guard-level sweep, simulator injection, noise run, timing).
---
1. Summary
In the simulation, every injected fault in the tested set reaches the detector in the first evaluation cycle after injection. This is a smoke test, not a detection-performance figure: the fault is applied to the detector input in the same pass that evaluates it, so first-cycle detection holds by construction. The 10 ms below is that one cycle at the assumed cycle period; it is not a measured hardware latency. No FPGA, flight processor or real-time operating system is involved.
The detector logic itself is formally proved against its specification (`satellite_fdir.bio`) for all float64 inputs; see the Formal Verification section of this bundle.
---
2. Smoke-test results (simulation)
| Metric | GPS Spoofing | Solar Panel Failure | Battery Failure |
|---|---|---|---|
| Cycles to detect | 1 | 1 | 1 |
| TTD (cycles × assumed 10 ms period) | 10.0 ms | 10.0 ms | 10.0 ms |
| Detection rate (100 runs) | 100% | 100% | 100% |
| Missed detections | 0 | 0 | 0 |
Note: the 100 runs (seeded, one seed per run) give identical results, so they are not an independent statistical sample. GPS: `gps_error` is written as a step; solar and battery: the model's failure injection is used and the battery level / generation attributes are set as in the web app glue. No synthetic hardware latency or jitter is added.
---
3. Metric definitions & limits
3.1 Time To Detection (TTD)
The number of simulation cycles between fault injection and assertion of the `anomaly_detected` flag, multiplied by the assumed cycle period (10 ms). It says nothing about real hardware timing.3.2 Software decision cost
One evaluation of the detector guard (`fdir_guard.detect`) takes about 400-500 ns median in CPython on a desktop OS (`measure_fdir_detection.py`, 5 repeats of 200000 calls). The tail is not stable: p99 ranged from 0.5 to 7.8 µs and the maximum from 56 to 711 µs between repeats of the same run, so no p99 figure is claimed. This bounds the software decision time on that machine only.3.3 False Alarm Rate (FAR)
3.4 Time To Isolation (TTI)
In the simulation the fault code is produced by the same function call as the detection, so isolation takes the same cycle. This is a software property, not a measured system figure.---
4. Comparison with a legacy EKF
No measured comparison exists. The EKF in the simulation is a scripted confidence-decay model, so a speed-up factor against it would not be evidence. No improvement factor is claimed.
Formal Verification (Z3): Detector Logic
System: MetaSpace.bio FDIR detector guard Status: machine-checked proof of implementation conformance to the specification. Reproduce with `python verify_guard_conformance.py`.
---
1. What is proved
The detector function `backend/modules/fdir_guard.py` (used by the simulator for GPS and IMU fault decisions) is proved, with the Z3 SMT solver over IEEE-754 float64 arithmetic, to conform to the formal specification `satellite_fdir.bio` for every possible input, including infinities and NaN:
| ID | Property |
|---|---|
| S1-S5 | For each of the five channels: residual magnitude at or above the `.bio` threshold implies `fault_detected` |
| S6 | All channels below their thresholds implies no fault (no false alarm) |
| S7 | `fault_detected` implies `safe_mode` |
| S8 | Any NaN input implies `fault_detected` (fail-safe on invalid sensor data) |
| S9 | `fault_code` is in 0..5 and is non-zero exactly when a fault is detected |
| S10-S14 | If only channel i is breached, the fault code identifies channel i |
| S15 | A nominal input vector is accepted (the specification is not over-constrained) |
The thresholds are parsed from the `.bio` file, and the guard carries independent constants, so any drift between the two is caught as a counterexample.
2. How the proof is made trustworthy
3. What is NOT proved
4. Earlier finding fixed by this work
The earlier `>` comparisons in the simulator did not trigger on a NaN sensor value and differed from the specification's `>=` at the exact threshold. The guard fixes both, and the proof covers them.
PFD Arithmetic (Illustrative, no SIL claimed)
System: MetaSpace.bio FDIR Architecture assumed: 1oo2 (One-out-of-Two) redundant system — a design target, not implemented in this repository Status: illustrative arithmetic on ASSUMED placeholder inputs. Not a measurement, not an assessment by an accredited body, not a certification, and no SIL is claimed.
---
1. Method
A simplified low-demand 1oo2 form in the style of IEC 61508-6, with detected failures neglected:
PFD_avg = (lambda_DU * T)^2 / 3 + beta * lambda_DU * T / 2 lambda_DU = lambda_total * (1 - DC)
The diagnostic coverage therefore does enter the result. An earlier revision of this document applied the common-cause factor to `lambda_total` (`beta x lambda_total x T / 2` = 5.58e-04); that form ignored the diagnostic coverage and is retired.
---
2. Inputs (all ASSUMED placeholders)
| Parameter | Symbol | Value | Basis |
|---|---|---|---|
| Total failure rate | lambda_total | 850 FIT (8.50e-7 per hour) | Placeholder rates for GPS receiver, IMU, CPU, power bus. No handbook look-up was done. These are the rates of the monitored units, not of the FDIR function |
| Diagnostic coverage | DC | 0.99 (nominal point) | Assumed target, varied below |
| Proof test interval | T | 3 years (26 280 h) | Assumed |
| Common cause beta factor | beta | 0.05 (nominal point) | Assumed, varied below |
---
3. Result and sensitivity
At the nominal assumed point the formula gives PFD_avg = 5.60e-06. The same placeholder rates give very different results when the assumed coverage and beta change:
| DC | beta | PFD_avg | IEC 61508-1 low-demand band (PFD alone) |
|---|---|---|---|
| 0.60 | 0.02 | 1.16e-04 | SIL 3 band |
| 0.60 | 0.05 | 2.50e-04 | SIL 3 band |
| 0.60 | 0.10 | 4.73e-04 | SIL 3 band |
| 0.90 | 0.02 | 2.40e-05 | SIL 4 band |
| 0.90 | 0.05 | 5.75e-05 | SIL 4 band |
| 0.90 | 0.10 | 1.13e-04 | SIL 3 band |
| 0.99 | 0.02 | 2.25e-06 | below the SIL 4 band (<1e-5) |
| 0.99 | 0.05 | 5.60e-06 | below the SIL 4 band (<1e-5) |
| 0.99 | 0.10 | 1.12e-05 | SIL 4 band |
The band ranges from the SIL 3 band to below the SIL 4 band for inputs that are all equally unmeasured, so the number says nothing about a SIL.
---
4. What would be needed for a SIL claim
None of these exist yet. The correct wording is "SIL 3 targeted".
Test Specifications & Robustness Analysis
System: MetaSpace.bio FDIR Date: 2026-10-31
---
1. Test Specifications
The following specifications define the conditions of the simulation runs. They are simulation conditions, not flight-hardware conditions.
1.1 Global Parameters
1.2 Test Cases (TC)
#### TC-GPS-01: GPS Spoofing Injection
#### TC-SOLAR-01: Solar Panel Failure
#### TC-BATT-01: Critical Battery Failure
---
2. Robustness Analysis
Robustness is the ability of the FDIR system to distinguish between Faults and Nominal Disturbances (Noise, Jitter).
2.1 Noise Immunity Thresholds
The Invariant Observers utilize "Gap Thresholds" to filter out sensor noise.| Sensor | Noise Floor (3σ) | FDIR Threshold | Margin Factor |
|---|---|---|---|
| GPS Position | ±5 m | ±50 m | 10x |
| Power Bus | ±5 W | ±500 W | 100x |
| Attitude | ±0.01° | ±0.5° | 50x |
Conclusion: The thresholds leave a margin of at least 10x over the documented noise floor. These noise floors are assumptions; they have not been measured on real sensors. With seeded Gaussian noise, 200 000 nominal cycles produced 0 false alarms (`measure_fdir_detection.py`); the run uses the tabulated values as the standard deviation (more severe than a 3σ reading), and the wheel (0.005 N·m) and battery (0.05 V) deviations are illustrative. The guard is also proved to give no fault whenever every channel is below its threshold.
2.2 Sensitivity Analysis
---
3. Configuration Management
The reproducing commands are listed in `CLAIMS_LEDGER.md` (the test cases run with `python -m unittest backend.tests.test_fdir_cases`); results depend on the repository commit and the Python/Z3 versions recorded in the generated reports.