park07/amradioСистема радиовещания на 12 каналах АМ на базе ПЛИС с формальной верификацией аппаратного сторожевого таймера для отказоустойчивой передачи аварийных оповещений в безлюдных туннелях.
12-канальная система AM-радиовещания на базе ПЛИС Red Pitaya для передачи экстренных оповещений в необслуживаемых туннелях.
Почему AM-радио в туннеле? Во время строительства и обслуживания автомобили со стандартными AM-радиоприемниками проезжают через туннели, где нет мобильной связи. AM-сигналы распространяются вдоль конструкций туннеля через кабели излучающего фидера, а приемники дешевы, надежны и уже есть в каждом автомобиле. Система передает заранее записанные экстренные оповещения на нескольких частотах, чтобы любой AM-радиоприемник, настроенный на любую станцию в диапазоне, получил сообщение. Аппаратный сторожевой таймер гарантирует отключение ВЧ-выхода при сбое системы управления — потому что автоматический перезапуск передатчика в необслуживаемом туннеле является неприемлемым режимом отказа.
| Функция | Статус |
|---|---|
| 12 одновременных несущих частот | ✅ |
| Настройка частоты во время выполнения (без изменений аппаратуры) | ✅ |
| AM-модуляция с предварительно записанным аудио | ✅ |
| Динамическое регулирование мощности | ✅ |
| Архитектура MVC (Rust + JavaScript) | ✅ |
| Событийно-ориентированная издатель-подписчик через шину событий | ✅ |
| UI без состояния — устройство как источник истины | ✅ |
| Сетевой опрос и автоматическое переподключение | ✅ |
| Безопасный аппаратный сторожевой таймер (тайм-аут 5 с) | ✅ |
| Формальная верификация (14 свойств, 6 покрытий, все доказаны) | ✅ |
model.rs): NetworkManager управляет TCP/SCPI, состоянием устройства, опросом каждые 500 мс, автоматическим переподключением с экспоненциальной задержкойview.js, index.html): Без состояния — отображает только подтвержденное состояние устройства. Никогда не предполагает состояние аппаратуры.controller.js): Обрабатывает ввод пользователя, публикует события в шинуevent_bus.rs, event_bus.js): Компоненты общаются через центральную шину вместо прямого вызова друг друга. Rust отправляет события клиентской части JS через мост Tauri.state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Промежуточные состояния предотвращают недопустимые переходы.wd.v): Аппаратный предохранитель — если сигнал от GUI прекращается на 5 секунд, ВЧ-выход отключается и фиксируется. Только ручной сброс оператора восстанавливает выход.am_scpi_server.py): Запускается на Red Pitaya, разбирает текстовые команды, преобразует частоты в приращения фазы, записывает в регистры ПЛИС через /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
---
## Формальная верификация
Сторожевой таймер математически доказан корректным с помощью bounded model checking и k-индукции (SymbiYosys + Z3 SMT solver). В отличие от симуляционного тестирования, которое проверяет отдельные сценарии, формальная верификация доказывает корректность для **каждого возможного входа, в каждом возможном состоянии, на все времена**.
### 14 Свойств безопасности (Все PASS)
| Категория | # | Свойство | Гарантия |
|-----------|---|----------|----------|
| **Базовые** | 1 | Сброс очищает все | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat предотвращает срабатывание | Heartbeat сбрасывает счетчик, очищает triggered и warning |
| | 6 | Отключение останавливает все | `!enable` → все выходы очищены |
| | 7 | Счетчик ограничен | Счетчик никогда не превышает TIMEOUT_CYCLES |
| | 8 | Принудительный сброс работает | `force_reset` очищает все состояния |
| | 9 | Предупреждение низко до порога | counter < WARNING_CYCLES → warning=0 |
| **Безопасность** | 3 | **Нет раннего срабатывания** | **triggered ТОЛЬКО когда counter ≥ TIMEOUT_CYCLES** |
| | 4 | Срабатывание гарантировано при тайм-ауте | Живучесть: по истечении времени всегда срабатывает trigger |
| | 5 | Предупреждение перед срабатыванием | triggered=1 → warning=1 |
| | 5b | Обратное утверждение | !warning → !triggered |
| | 10 | Предупреждение высоко в зоне | counter > WARNING_CYCLES → warning=1 |
| | 11 | Счетчик увеличивается корректно | Ровно +1 за такт во время счета |
| **Выход** | 12 | time_remaining при нуле | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining при срабатывании | triggered → time_remaining = 0 |
| | 14 | time_remaining монотонно | Уменьшается каждый цикл во время счета |
### 6 Сценариев покрытия (Все достигнуты)
| # | Сценарий | Шаги | Описание |
|---|----------|------|----------|
| 1 | Срабатывание триггера | 23 | Счетчик достигает тайм-аута |
| 2 | Предупреждение без срабатывания | 21 | В зоне предупреждения, еще не тайм-аут |
| 3 | Точная граница тайм-аута | 22 | Счетчик = TIMEOUT_CYCLES точно |
| 4 | Heartbeat в последний момент | 19 | Heartbeat при счетчике = T-1 |
| 5 | Восстановление после срабатывания | 24 | Состояние срабатывания сброшено force_reset |
| 6 | Жизненный цикл предупреждение-срабатывание | 23 | Предупреждение, затем немедленное срабатывание |
### Запуск верификации```bash
cd fpga/formal/
sby -f wd.sby
Ожидаемый результат:
```
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.
### Масштабируемость
Верификация использует `CLK_FREQ=1`, `TIMEOUT_SEC=5` для обеспечения управляемости пространства состояний. В производстве используется `CLK_FREQ=125000000`. RTL параметризован — та же логика if/else, те же переходы состояний. Доказательство в уменьшенном масштабе подразумевает корректность в производственном масштабе.
См. [`fpga/formal/README.md`](https://github.com/park07/amradio/blob/main/am_radio/fpga/formal/README.md)
---
## Требования
### Оборудование
- Red Pitaya STEMlab 125-10
- AM радиоприемник(и) для тестирования
- Ethernet-кабель (для подключения Red Pitaya)
### Программное обеспечение