park07/amradioنظام بث إذاعي AM بـ 12 قناة يعتمد على FPGA مع التحقق الرسمي من مراقب العتاد لنقل تنبيهات الطوارئ بشكل آمن ضد الفشل في الأنفاق غير المأهولة.
نظام بث راديو AM مكون من 12 قناة يستخدم Red Pitaya FPGA لنقل التنبيهات الطارئة في الأنفاق غير المأهولة.
لماذا راديو AM في النفق؟ أثناء الإنشاء والصيانة، تمر المركبات المزودة بأجهزة راديو AM القياسية عبر أنفاق لا تغطيها شبكات الهاتف المحمول. تنتشر إشارات AM على طول هياكل الأنفاق عبر كابلات leaky feeder، كما أن أجهزة الاستقبال رخيصة ومتينة وموجودة بالفعل في كل مركبة. يبث النظام تنبيهات طارئة مسجلة مسبقًا عبر ترددات متعددة بحيث أي راديو AM مضبوط على أي محطة في النطاق سيستقبل الرسالة. يعمل مؤقت مراقبة (watchdog) على إيقاف خرج التردد اللاسلكي إذا فشل نظام التحكم — لأن إعادة تشغيل جهاز الإرسال تلقائيًا في نفق غير مأهول ليس نمط فشل مقبولًا.
| الميزة | الحالة |
|---|---|
| 12 تردد حامل متزامن | ✅ |
| تكوين التردد أثناء التشغيل (بدون تغييرات في الأجهزة) | ✅ |
| تضمين AM مع صوت مسجل مسبقًا | ✅ |
| تدرج القدرة الديناميكي | ✅ |
| هندسة MVC (Rust + JavaScript) | ✅ |
| نشر/اشتراك قائم على الأحداث عبر ناقل الأحداث | ✅ |
| واجهة مستخدم بدون حالة — الجهاز هو مصدر الحقيقة | ✅ |
| الاستقصاء الشبكي وإعادة الاتصال التلقائي | ✅ |
| مؤقت مراقبة أجهزة آمن من الفشل (مهلة 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): آمن من الفشل في الأجهزة — إذا توقف نبض واجهة المستخدم لمدة 5 ثوانٍ، يتم إيقاف خرج التردد اللاسلكي وتثبيته. فقط إعادة تعيين يدوية بواسطة المشغل تعيد الخرج.am_scpi_server.py): يعمل على Red Pitaya، يحلل الأوامر النصية، يحول الترددات إلى زيادات طور، يكتب إلى سجلات FPGA عبر /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 (k-induction) (SymbiYosys + محلل Z3 SMT). على عكس الاختبار القائم على المحاكاة الذي يفحص سيناريوهات فردية، يثبت التحقق الرسمي الصحة عبر **كل مدخل ممكن، في كل حالة ممكنة، لكل الأوقات**.
### 14 خاصية سلامة (جميعها ناجحة)
| الفئة | # | الخاصية | الضمان |
|----------|------|----------|-----------|
| **أساسي** | 1 | إعادة التعيين تمسح الكل | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | النبض القلبي يمنع التفعيل | النبض القلبي يعيد ضبط العداد، ويمسح triggered و warning |
| | 6 | التعطيل يلغي كل شيء | `!enable` → جميع المخرجات ممسوحة |
| | 7 | العداد محدود | العداد لا يتجاوز TIMEOUT_CYCLES |
| | 8 | إعادة التعيين القسري تعمل | `force_reset` تمسح كل الحالة |
| | 9 | التحذير منخفض قبل العتبة | counter < WARNING_CYCLES → warning=0 |
| **سلامة** | 3 | **لا تفعيل مبكر** | **triggered فقط عندما counter ≥ TIMEOUT_CYCLES** |
| | 4 | التفعيل مضمون عند المهلة | الحيوية: المهلة دائمًا تشغل التفعيل |
| | 5 | تحذير قبل التفعيل | triggered=1 → warning=1 |
| | 5ب | المعاكس | !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 | نبض قلبي في اللحظة الأخيرة | 19 | نبض قلبي عند العداد = 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 للاختبار
- كابل إيثرنت (لتوصيل Red Pitaya)
### البرمجيات
| التبعية | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | قم بتنزيل `rustup-init.exe` من [rustup.rs](https://rustup.rs) |
| Node.js (LTS) | `brew install node` أو [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode Command Line Tools (لـ macOS فقط) | `xcode-select --install` | — |
| Visual Studio Build Tools (لـ Windows فقط) | — | [تحميل](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — اختر **"تطوير سطح المكتب باستخدام C++"** |
### التحقق الرسمي (اختياري)
- SymbiYosys
- Yosys
- محلل Z3 SMT
---
## التثبيت
### 1. استنساخ المستودع```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh source $HOME/.cargo/env
xcode-select --install
brew install node
cd gui npm install npm run build
التطبيق المبني `.app` سيكون في `gui/src-tauri/target/release/bundle/macos/`.
#### ويندوز (PowerShell)```powershell
# 1. Install Rust
# Download and run rustup-init.exe from https://rustup.rs
# Close and reopen PowerShell after install