park07/amradioSystème de diffusion radio AM à 12 canaux basé sur FPGA avec vérification formelle d’un watchdog matériel pour la transmission d’alertes d’urgence à sécurité intégrée dans les tunnels sans personnel.
Un système de radiodiffusion AM à 12 canaux utilisant le FPGA Red Pitaya pour la transmission d'alertes d'urgence dans les tunnels sans personnel.
Pourquoi la radio AM dans un tunnel ? Pendant la construction et la maintenance, les véhicules équipés de radios AM standard traversent des tunnels sans couverture mobile. Les signaux AM se propagent le long des structures du tunnel via des câbles rayonnants, et les récepteurs sont bon marché, robustes et déjà présents dans chaque véhicule. Le système diffuse des alertes d'urgence préenregistrées sur plusieurs fréquences afin que toute radio AM réglée sur n'importe quelle station de la bande reçoive le message. Un chien de garde matériel garantit que la sortie RF est coupée si le système de contrôle échoue — car le redémarrage automatique d'un émetteur dans un tunnel sans personnel n'est pas un mode de défaillance acceptable.
| Fonctionnalité | Statut |
|---|---|
| 12 fréquences porteuses simultanées | ✅ |
| Configuration des fréquences en temps réel (sans modification matérielle) | ✅ |
| Modulation AM avec audio préenregistré | ✅ |
| Ajustement dynamique de la puissance | ✅ |
| Architecture MVC (Rust + JavaScript) | ✅ |
| Pub/sous événementiel via bus d'événements | ✅ |
| UI sans état — le dispositif est source de vérité | ✅ |
| Sondage réseau & reconnexion automatique | ✅ |
| Chien de garde matériel à sécurité intégrée (délai de 5 s) | ✅ |
| Vérification formelle (14 propriétés, 6 couvertures, toutes prouvées) | ✅ |
model.rs) : NetworkManager gère TCP/SCPI, l'état du dispositif, le sondage à 500 ms, la reconnexion automatique avec backoff exponentielview.js, index.html) : Sans état — n'affiche que l'état confirmé du dispositif. Ne présuppose jamais l'état matériel.controller.js) : Gère les entrées utilisateur, publie des événements sur le busevent_bus.rs, event_bus.js) : Les composants communiquent via un bus central au lieu de s'appeler directement. Rust émet des événements vers le frontend JS via le pont Tauri.state_machine.rs) : IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Les états intermédiaires empêchent les transitions invalides.wd.v) : Sécurisé en matériel — si le battement de cœur de l'interface utilisateur s'arrête pendant 5 secondes, la sortie RF est coupée et verrouillée. Seule une réinitialisation manuelle par l'opérateur rétablit la sortie.am_scpi_server.py) : S'exécute sur le Red Pitaya, analyse les commandes textuelles, convertit les fréquences en incréments de phase, écrit dans les registres FPGA via /dev/mem.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
---
## Vérification formelle
Le chien de garde (watchdog) est mathématiquement prouvé correct en utilisant le model checking borné et l'induction-k (SymbiYosys + solveur SMT Z3). Contrairement aux tests basés sur la simulation qui vérifient des scénarios individuels, la vérification formelle prouve l'exactitude pour **chaque entrée possible, dans chaque état possible, pour toujours**.
### 14 Propriétés de sécurité (Toutes réussies)
| Catégorie | # | Propriété | Garantie |
|----------|---|----------|-----------|
| **Basique** | 1 | Reset efface tout | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat empêche le déclenchement | Heartbeat réinitialise le compteur, efface triggered et warning |
| | 6 | Désactivation arrête tout | `!enable` → toutes les sorties effacées |
| | 7 | Compteur borné | Le compteur ne dépasse jamais TIMEOUT_CYCLES |
| | 8 | Force reset fonctionne | `force_reset` efface tout l'état |
| | 9 | Avertissement bas avant seuil | counter < WARNING_CYCLES → warning=0 |
| **Sécurité** | 3 | **Pas de déclenchement prématuré** | **déclenché UNIQUEMENT quand counter ≥ TIMEOUT_CYCLES** |
| | 4 | Déclenchement garanti à l'expiration du délai | Vivacité : le délai déclenche toujours |
| | 5 | Avertissement avant déclenchement | triggered=1 → warning=1 |
| | 5b | Contraposée | !warning → !triggered |
| | 10 | Avertissement élevé dans la zone | counter > WARNING_CYCLES → warning=1 |
| | 11 | Compteur s'incrémente correctement | Exactement +1 par cycle d'horloge pendant le comptage |
| **Sortie** | 12 | time_remaining à zéro | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining au déclenchement | triggered → time_remaining = 0 |
| | 14 | time_remaining monotone | Diminue à chaque cycle pendant le comptage |
### 6 Scénarios de couverture (Tous atteints)
| # | Scénario | Pas | Description |
|---|----------|-------|-------------|
| 1 | Déclenchement se produit | 23 | Le compteur atteint le délai |
| 2 | Avertissement sans déclenchement | 21 | Dans la zone d'avertissement, pas encore expiré |
| 3 | Limite exacte du délai | 22 | Compteur = TIMEOUT_CYCLES exactement |
| 4 | Heartbeat de dernière seconde | 19 | Heartbeat au compteur = T-1 |
| 5 | Récupération après déclenchement | 24 | État déclenché effacé par force_reset |
| 6 | Cycle de vie avertissement-déclenchement | 23 | Avertissement puis déclenchement immédiat |
### Exécution de la vérification```bash
cd fpga/formal/
sby -f wd.sby
Sortie attendue:
```
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.
### Passage à l'échelle
La vérification utilise `CLK_FREQ=1`, `TIMEOUT_SEC=5` pour garder l'espace d'état traitable. La production utilise `CLK_FREQ=125000000`. Le RTL est paramétré — même logique if/else, mêmes transitions d'état. Une preuve à échelle réduite implique la correction à l'échelle de production.
Voir [`fpga/formal/README.md`](https://github.com/park07/amradio/blob/main/am_radio/fpga/formal/README.md)
---
## Prérequis
### Matériel
- Red Pitaya STEMlab 125-10
- Récepteur(s) radio AM pour les tests
- Câble Ethernet (pour la connexion Red Pitaya)
### Logiciel