park07/amradioFPGA-basiertes 12-Kanal-AM-Rundfunksystem mit formaler Verifikation eines Hardware-Watchdogs für die ausfallsichere Notfallwarnübertragung in unbemannten Tunneln.
Ein 12-Kanal AM-Rundfunksystem, das die Red Pitaya FPGA zur Übermittlung von Notfallwarnungen in unbemannten Tunneln nutzt.
Warum AM-Radio in einem Tunnel? Während Bau- und Wartungsarbeiten durchfahren Fahrzeuge mit serienmäßigen AM-Radios Tunnel, die keine Mobilfunkabdeckung haben. AM-Signale breiten sich entlang der Tunnelstrukturen über Leaky-Feeder-Kabel aus, und die Empfänger sind günstig, robust und in jedem Fahrzeug bereits vorhanden. Das System sendet vorab aufgezeichnete Notfallwarnungen auf mehreren Frequenzen aus, sodass jedes AM-Radio, das auf einen Sender im Band eingestellt ist, die Nachricht empfängt. Ein Hardware-Watchdog stellt sicher, dass die HF-Leistung abgeschaltet wird, falls das Steuerungssystem ausfällt – denn ein automatischer Neustart eines Senders in einem unbemannten Tunnel ist keine akzeptable Fehlerart.
| Funktion | Status |
|---|---|
| 12 gleichzeitige Trägerfrequenzen | ✅ |
| Laufzeit-Frequenzkonfiguration (keine Hardware-Änderungen) | ✅ |
| AM-Modulation mit vorab aufgezeichnetem Audio | ✅ |
| Dynamische Leistungsanpassung | ✅ |
| MVC-Architektur (Rust + JavaScript) | ✅ |
| Ereignisgesteuertes Pub/Sub über Event-Bus | ✅ |
| Zustandslose Benutzeroberfläche – das Gerät ist die Quelle der Wahrheit | ✅ |
| Netzwerk-Polling & automatische Wiederverbindung | ✅ |
| Ausfallsicherer Hardware-Watchdog (5s Timeout) | ✅ |
| Formale Verifikation (14 Eigenschaften, 6 Covers, alle bewiesen) | ✅ |
model.rs): NetworkManager verwaltet TCP/SCPI, Gerätezustand, 500ms Polling, automatische Wiederverbindung mit exponentiellem Backoffview.js, index.html): Zustandslos – rendert nur bestätigten Gerätezustand. Nimmt niemals Hardware-Zustand an.controller.js): Verarbeitet Benutzereingaben, veröffentlicht Ereignisse auf dem Busevent_bus.rs, event_bus.js): Komponenten kommunizieren über einen zentralen Bus anstatt direkt aufzurufen. Rust emittiert Ereignisse an das JS-Frontend über die Tauri-Brücke.state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Zwischenzustände verhindern ungültige Übergänge.wd.v): Hardware-Failsafe – wenn der GUI-Heartbeat für 5 Sekunden ausbleibt, wird die HF-Leistung abgeschaltet und verriegelt. Nur ein manueller Reset durch den Bediener stellt die Ausgabe wieder her.am_scpi_server.py): Läuft auf der Red Pitaya, parst Textbefehle, wandelt Frequenzen in Phaseninkremente um, schreibt über /dev/mem in FPGA-Register.GUI click → invoke("set_frequency") → model.rs sends "FREQ:CH1 700000" over TCP → am_scpi_server.py converts to phase_inc = (700000 × 2³²) / 125MHz → writes to FPGA register via /dev/mem → NCO generates carrier → AM modulates → RF output
---
## Formale Verifikation
Der Watchdog-Timer ist mathematisch korrekt nachgewiesen mithilfe von Bounded Model Checking und k-Induktion (SymbiYosys + Z3 SMT-Löser). Im Gegensatz zum simulationsbasierten Testen, das einzelne Szenarien überprüft, beweist die formale Verifikation die Korrektheit für **jede mögliche Eingabe, in jedem möglichen Zustand, für alle Zeit**.
### 14 Sicherheitseigenschaften (Alle BESTANDEN)
| Kategorie | # | Eigenschaft | Garantie |
|-----------|---|-------------|----------|
| **Grundlegend** | 1 | Reset löscht alles | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat verhindert Auslösung | Heartbeat setzt Zähler zurück, löscht triggered und warning |
| | 6 | Deaktivieren beendet alles | `!enable` → alle Ausgänge gelöscht |
| | 7 | Zähler begrenzt | Zähler überschreitet nie TIMEOUT_CYCLES |
| | 8 | Forcierter Reset funktioniert | `force_reset` löscht den gesamten Zustand |
| | 9 | Warnung niedrig vor Schwelle | counter < WARNING_CYCLES → warning=0 |
| **Sicherheit** | 3 | **Keine vorzeitige Auslösung** | **triggered NUR wenn counter ≥ TIMEOUT_CYCLES** |
| | 4 | Auslösung garantiert bei Timeout | Lebendigkeit: Timeout löst immer trigger aus |
| | 5 | Warnung vor Auslösung | triggered=1 → warning=1 |
| | 5b | Kontraposition | !warning → !triggered |
| | 10 | Warnung hoch in Zone | counter > WARNING_CYCLES → warning=1 |
| | 11 | Zähler inkrementiert korrekt | Genau +1 pro Taktzyklus während des Zählens |
| **Ausgang** | 12 | time_remaining bei Null | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining bei Auslösung | triggered → time_remaining = 0 |
| | 14 | time_remaining monoton | Nimmt jeden Zyklus während des Zählens ab |
### 6 Abdeckungsszenarien (Alle erreicht)
| # | Szenario | Schritte | Beschreibung |
|---|----------|----------|--------------|
| 1 | Auslösung erfolgt | 23 | Zähler erreicht Timeout |
| 2 | Warnung ohne Auslösung | 21 | In Warnzone, noch nicht abgelaufen |
| 3 | Exakte Timeout-Grenze | 22 | Zähler = TIMEOUT_CYCLES genau |
| 4 | Heartbeat in letzter Sekunde | 19 | Heartbeat bei Zähler = T-1 |
| 5 | Wiederherstellung nach Auslösung | 24 | Ausgelöster Zustand durch force_reset gelöscht |
| 6 | Warnungs-zu-Auslösung-Lebenszyklus | 23 | Warnung dann sofortige Auslösung |
### Ausführen der Verifikation```bash
cd fpga/formal/
sby -f wd.sby
Erwartete Ausgabe:
```
SBY [wd_prove] DONE (PASS, rc=0)
summary: successful proof by k-induction.
SBY [wd_cover] DONE (PASS, rc=0)
summary: 6/6 cover statements reached.
### Skalierbarkeit
Die Verifikation verwendet `CLK_FREQ=1`, `TIMEOUT_SEC=5`, um den Zustandsraum handhabbar zu halten. In der Produktion wird `CLK_FREQ=125000000` verwendet. Das RTL ist parametrisiert – gleiche if/else-Logik, gleiche Zustandsübergänge. Ein Beweis im reduzierten Maßstab impliziert Korrektheit im Produktionsmaßstab.
Siehe [`fpga/formal/README.md`](https://github.com/park07/amradio/blob/main/am_radio/fpga/formal/README.md)
---
## Anforderungen
### Hardware
- Red Pitaya STEMlab 125-10
- AM-Radioempfänger zum Testen
- Ethernet-Kabel (für Red Pitaya-Verbindung)
### Software