نظام الاختراق عبر راديو AM

نظام بث راديو AM مكون من 12 قناة يستخدم Red Pitaya FPGA لنقل التنبيهات الطارئة في الأنفاق غير المأهولة.

لماذا راديو AM في النفق؟ أثناء الإنشاء والصيانة، تمر المركبات المزودة بأجهزة راديو AM القياسية عبر أنفاق لا تغطيها شبكات الهاتف المحمول. تنتشر إشارات AM على طول هياكل الأنفاق عبر كابلات leaky feeder، كما أن أجهزة الاستقبال رخيصة ومتينة وموجودة بالفعل في كل مركبة. يبث النظام تنبيهات طارئة مسجلة مسبقًا عبر ترددات متعددة بحيث أي راديو AM مضبوط على أي محطة في النطاق سيستقبل الرسالة. يعمل مؤقت مراقبة (watchdog) على إيقاف خرج التردد اللاسلكي إذا فشل نظام التحكم — لأن إعادة تشغيل جهاز الإرسال تلقائيًا في نفق غير مأهول ليس نمط فشل مقبولًا.

الميزات

البنية

طبقة البرمجيات

• الإطار: خلفية Rust (Tauri) + واجهة أمامية JavaScript
• البنية: MVC مع نشر/اشتراك قائم على الأحداث
• النموذج (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. الحالات الوسيطة تمنع الانتقالات غير الصالحة.
• مصدر الحقيقة: الجهاز وليس البرمجيات. يتم تحديث واجهة المستخدم فقط بعد تأكيد الأجهزة.

طبقة الأجهزة

• NCO: 12 مذبذبًا مُتحكمًا به رقميًا يولد ترددات الحامل (505–1605 kHz)
• مُضمن AM: يدمج مصدر الصوت مع كل حامل
• التدرج الديناميكي: يتم ضبط طاقة الخرج بناءً على عدد القنوات المفعلة
• مخزن الصوت المؤقت: BRAM يخزن رسائل طارئة مسجلة مسبقًا (مخزن مؤقت 16,384 عينة بمعدل تشغيل ~5 كيلو هرتز). يتوفر مُحمِّل صوت AXI للتحميل أثناء التشغيل.
• مؤقت المراقبة (wd.v): آمن من الفشل في الأجهزة — إذا توقف نبض واجهة المستخدم لمدة 5 ثوانٍ، يتم إيقاف خرج التردد اللاسلكي وتثبيته. فقط إعادة تعيين يدوية بواسطة المشغل تعيد الخرج.
• خادم SCPI (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

2. بناء واجهة المستخدم الرسومية

macOS```bash

Install Rust (if not installed)

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh source $HOME/.cargo/env

Install Xcode CLI tools (if not installed)

xcode-select --install

Install Node.js via Homebrew (if not installed)

brew install node

Build

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

# 2. Install Visual Studio Build Tools
#    Download from https://visualstudio.microsoft.com/visual-cpp-build-tools/
#    Select "Desktop development with C++" during installation
#    Close and reopen PowerShell after install

# 3. Install Node.js
#    Download LTS from https://nodejs.org
#    Close and reopen PowerShell after install

# 4. Verify installations
rustc --version
cargo --version
node --version
npm --version

# 5. Build
cd gui
npm install
npm run build

سيكون الملف .exe المبني في gui\src-tauri\target\release\.

ملاحظة: يستغرق البناء الأول حوالي 2-3 دقائق (تجميع Rust). البناءات التالية أسرع.

3. إعداد Red Pitaya

قم بالاتصال عبر SSH بـ Red Pitaya:```bash ssh root@<RED_PITAYA_IP>

Default password: root

انسخ الملفات المطلوبة:```bash

scp am_scpi_server.py root@<RED_PITAYA_IP>:/root/
scp axi_audio_sequence_loop.py root@<RED_PITAYA_IP>:/root/
scp alarm_fast.wav 0009_part1.wav 0009_part2_fast.wav root@<RED_PITAYA_IP>:/root/
scp fpga/red_pitaya_top.bit root@<RED_PITAYA_IP>:/root/

ملاحظة

Bitstream موجود بالفعل على بطاقة SD الخاصة بـ Red Pitaya من التطوير.

لإعادة البناء: افتح project_William.xpr في Vivado، قم بتوليد bitstream، ثم استخدم scp لنقل ملف .bit الجديد إلى Red Pitaya.

4. بيئة بايثون (Red Pitaya)

يدير Red Pitaya نظام Alpine Linux مع Python 3.5. خادم SCPI ليس له تبعيات خارجية (stdlib فقط). يتطلب محمل الصوت numpy:```bash

On Red Pitaya

pip install numpy

> **ملاحظة:** لا يدعم إصدار Python 3.5 الخاص بـ Red Pitaya خاصية `venv` بشكل افتراضي، ويعمل كجذر (root)، لذا يتم تثبيت الحزم عالميًا. هذا مقبول — فهو جهاز مضمن، وليس خادمًا مشتركًا.

### 5. بيئة بايثون (تطوير محلي — اختياري)

إذا كنت ترغب في تشغيل أو تعديل نصوص بايثون محليًا (مثلًا لاختبار معالجة الصوت دون جهاز Red Pitaya):```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

أضف venv/ إلى .gitignore إذا لم يكن موجودًا بالفعل.

ملفات الصوت

يقوم النظام بتشغيل ثلاثة ملفات صوتية في حلقة: إنذار → الجزء 1 → الجزء 2 → (تكرار).

جميع الملفات الصوتية يتم تقليل تردد أخذ العينات إلى ~5 كيلوهرتز لتناسب مخزن BRAM بسعة 16,384 عينة في FPGA. يتولى سكريبت axi_audio_sequence_loop.py عملية إعادة التشكيل، والتحويل إلى 14 بت، والتحميل المتسلسل تلقائيًا.

الاستخدام

تحتاج إلى ثلاث محطات SSH مفتوحة إلى Red Pitaya، بالإضافة إلى محطة محلية واحدة لواجهة المستخدم الرسومية.

ملاحظة: قد يتغير عنوان IP الخاص بـ Red Pitaya في كل مرة يتم تشغيله. افحص قائمة عملاء DHCP في الموجه الخاص بك أو استخدم ping rp-f0866a.local للعثور عليه.

الخطوة 1: الاتصال بـ Red Pitaya

افتح محطة طرفية وأدخل عبر SSH:```bash ssh root@<RED_PITAYA_IP>

Password: root

### الخطوة ٢: تحميل تدفق البتات FPGA

على Red Pitaya (الطرفية الأولى SSH):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

يؤدي هذا إلى تحميل تصميم راديو AM على FPGA. مطلوب بعد كل دورة طاقة.

الخطوة 3: بدء خادم SCPI

على Red Pitaya (نفس المحطة الطرفية SSH أو الثانية):```bash python3 /root/am_scpi_server.py

اترك هذا قيد التشغيل — فهو يربط أوامر TCP من واجهة المستخدم الرسومية بسجلات FPGA.

### الخطوة 4: بدء حلقة الصوت

افتح محطة SSH ثانية إلى Red Pitaya:```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

الإخراج المتوقع:```

AXI AUDIO SEQUENCE - AUTO LOOP Alarm -> Part 1 -> Part 2 -> (repeat)

Buffer: 16384 samples FPGA playback rate: 5000 Hz Press Ctrl+C to stop

### الخطوة 5: تشغيل الواجهة الرسومية

على جهازك المحلي:```bash
cd gui
npm run dev

أو قم بتشغيل الثنائي المُجمّع مباشرةً من src-tauri/target/release/.

الخطوة 6: الاتصال والبث

1. أدخل عنوان IP الخاص بـ Red Pitaya
2. انقر على اتصال (Connect)
3. فعّل القنوات المطلوبة (1–12)
4. اضبط الترددات إذا لزم الأمر
5. انقر على بدء البث (START BROADCAST)
6. اضبط راديو AM على أي تردد مفعّل

Vivado (لتطوير FPGA فقط)

إذا كنت بحاجة إلى تعديل تصميم FPGA وإعادة بناء bitstream، فقم بتثبيت Vivado 2020.1. توفر Red Pitaya دليل إعداد هنا:

https://redpitaya.readthedocs.io/en/latest/developerGuide/fpga/getting_started/vivado_install.html

جميع الإعدادات والدروس الأساسية لـ Red Pitaya متوفرة على الوثائق الرسمية لـ Red Pitaya.

هيكل الملفات```

am_radio/ ├── gui/ │ ├── src/ │ │ ├── index.html # HTML + CSS │ │ └── js/ │ │ ├── event_bus.js # Frontend pub/sub + Tauri listener │ │ ├── model.js # Rust API calls (stateless) │ │ ├── view.js # DOM rendering │ │ └── controller.js # Event handlers │ └── src-tauri/src/ │ ├── main.rs # Entry point │ ├── model.rs # NetworkManager + DeviceState │ ├── commands.rs # Tauri command bridge │ ├── event_bus.rs # Rust pub/sub + Tauri emit │ ├── state_machine.rs # Broadcast state transitions │ └── config.rs # Constants ├── fpga/ │ ├── formal/ │ │ ├── wd.v # Watchdog + 14 formal properties │ │ ├── wd.sby # SymbiYosys config │ │ └── README.md # Formal verification docs │ ├── am_mod.sv # AM modulation module │ ├── am_radio_ctrl.v # 12-channel AM radio controller │ ├── axi_audio_buffer.v # AXI audio buffer for BRAM playback │ ├── nco_sin.v # Numerically Controlled Oscillator │ ├── red_pitaya_top.sv # Top-level FPGA integration │ ├── sine_lut_4096.mem # 4096-point sine lookup table │ └── watchdog_timer.v # Watchdog timer module (production) ├── am_scpi_server.py # SCPI server (runs on Red Pitaya) ├── axi_audio_sequence_loop.py # Audio sequence loader (alarm → part1 → part2 loop) ├── alarm_fast.wav # Alarm tone ├── 0009_part1.wav # Emergency message part 1 ├── 0009_part2_fast.wav # Emergency message part 2 ├── requirements.txt # Python dependencies (numpy) └── README.md

---

## ترددات القنوات (الافتراضية)

| القناة | التردد |
|---------|-----------|
| CH1 | 505 kHz |
| CH2 | 605 kHz |
| CH3 | 705 kHz |
| CH4 | 805 kHz |
| CH5 | 905 kHz |
| CH6 | 1005 kHz |
| CH7 | 1105 kHz |
| CH8 | 1205 kHz |
| CH9 | 1305 kHz |
| CH10 | 1405 kHz |
| CH11 | 1505 kHz |
| CH12 | 1605 kHz |

الترددات قابلة للتعديل أثناء التشغيل (نطاق 500–1700 كيلوهرتز).

---

## تصميم أمان المراقب (Watchdog)
![آلة حالة المراقب (Watchdog)](https://assets.kitploit.com/production/public/readmes/11878/6531091e26d450ab35e4e20c91ca2b88952b40ccf8a195443fe782cb413f45c5.png)```
Standard watchdog:  device hangs → timer overflows → restarts device → back to normal
This watchdog:      GUI dies → counter hits timeout → kills RF output → stays dead until operator resets

لماذا مختلف: إعادة تشغيل جهاز إرسال لاسلكي تلقائيًا في نفق غير مأهول أمر خطير. يتطلب النظام تأكيدًا بشريًا قبل استئناف خرج التردد اللاسلكي. آمن عند الفشل، وليس التعافي عند الفشل.

هامش الأمان: واجهة المستخدم تفحص كل 500 مللي ثانية. مهلة المراقبة 5 ثوان. ذلك يعني 10 نبضات مفقودة متتالية قبل التنشيط — مقاوم لتأخيرات الشبكة المؤقتة.

ملاحظات الأداء

التوصية: 4-5 قنوات كحد أقصى لاستقبال موثوق.

مرجع أوامر SCPI

الاختبارات

اختبارات الوحدة بلغة Rust

11 اختبارًا عبر الواجهة الخلفية — انتقالات آلة الحالة، النشر/الاشتراك في ناقل الأحداث، منطق إعادة المحاولة، والتحقق من التكوين.```bash cd gui/src-tauri cargo test

### التحقق الرسمي (FPGA)

14 خاصية سلامة مثبتة رياضياً على مؤقت المراقبة. راجع قسم [التحقق الرسمي](#formal-verification) أعلاه.

### الخادم الوهمي

لاختبار واجهة المستخدم الرسومية بدون توصيل Red Pitaya:```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

ثم اتصل بـ 127.0.0.1:5000 في واجهة المستخدم الرسومية.

استكشاف الأخطاء وإصلاحها

للمطورين المستقبليين

سيتم توريث هذا المشروع إلى الدفعة القادمة من EPI. إليك ما تحتاج معرفته.

ما يعمل

سلسلة الإشارة الكاملة تعمل: واجهة المستخدم الرسومية → الواجهة الخلفية Rust → TCP/SCPI → Red Pitaya → FPGA → خرج RF. يتم تشغيل الصوت تلقائيًا في حلقة. يقوم المراقب بإيقاف RF إذا انقطعت واجهة المستخدم الرسومية. تم عرض كل هذا مباشرة على العتاد.

ما يمكن تحسينه

مخزن الصوت المؤقت في FPGA محدود بـ 16,384 عينة في BRAM، مما يفرض تقليل معدل العينات إلى ~5 كيلوهرتز. الصوت الأطول أو الأعلى جودة سيحتاج إلى ذاكرة خارجية (DDR أو بطاقة SD). النص البرمجي axi_audio_sequence_loop.py يعيد تحميل الصوت عبر AXI بفجوة زمنية تبلغ ~1.4 ثانية بين المسارات — سيقضي DMA على ذلك. حاليًا فقط 4–5 قنوات عملية بقوة إشارة قابلة للاستخدام؛ مرحلة مضخم RF خارجية ستسمح بتشغيل جميع القنوات الـ12 في وقت واحد.

الملفات الرئيسية لفهمها أولاً

اقرأ model.rs (الواجهة الخلفية Rust — كل منطق الشبكة موجود هنا)، am_scpi_server.py (الجسر بين أوامر TCP ومسجلات FPGA)، و am_radio_ctrl.v (واجهة المسجلات بين البرمجيات والعتاد). هذه الملفات الثلاثة هي نقاط المصافحة بين كل طبقة من النظام.

الوصول إلى Red Pitaya

كان عنوان IP الخاص بـ Red Pitaya هو 192.168.0.101 أثناء التطوير. بيانات اعتماد SSH هي root/root. يتم تحميل دفق بت FPGA تلقائيًا عند التمهيد من بطاقة SD. إذا كان دفق البت مفقودًا أو تالفًا، فستحتاج إلى Vivado لإعادة بنائه من المصادر .sv/.v في fpga/.

سير عمل التطوير

لتغييرات واجهة المستخدم الرسومية: حرّر JS/HTML في gui/src/، شغّل npm run dev — يعيد تحميل الواجهة الأمامية تلقائيًا. لتغييرات الواجهة الخلفية Rust: حرّر الملفات في gui/src-tauri/src/، خادم التطوير يعيد الترجمة تلقائيًا (يستغرق بضع ثوانٍ). لتغييرات FPGA: حرّر Verilog في fpga/، قم بالتوليف في Vivado، أنشئ دفق بت جديد، انسخه إلى بطاقة SD الخاصة بـ Red Pitaya.

ملاحظة مهمة!:

• بالنسبة لعملي، كانت ملفات الصوت مخزنة بالفعل داخل Red Pitaya. وبما أنه يحتوي على مخزن ذاكرة مؤقت أقصى حجمه 32 كيلو، كان علينا تقسيم الصوت الطارئ إلى 3 أجزاء (حوالي 4 ثوانٍ لكل جزء)، وكان يعيد كتابة الصوت السابق.
• ملفات الصوت غير موجودة في هذا المستودع ولكن لا تتردد في اكتشاف ذلك. أوصي باستخدام إصدار Red Pitaya 14 لبث حي أفضل. الإصدار 125-10 قديم جدًا ومعظم مشاكل الذاكرة التي تم مواجهتها يمكن حلها بسهولة عن طريق الترقية إلى 125-15. لدى Pavel ملاحظة رائعة قد تكون ذات صلة أيضًا للإصدار 125-14.

المؤلفون

• ("Jaewoo") William Park (JW P) — بنية البرمجيات (واجهة المستخدم الرسومية، MVC، بنية تعتمد على الأحداث)، الواجهة الأمامية (JS)، الواجهة الخلفية (Rust)، مؤقت مراقب الجهاز، التحقق الرسمي، آلة الحالة
• Bowen Deng — تطوير FPGA (NCO، تعديل AM، خرج RF)

شكر وتقدير

• جامعة نيو ساوث ويلز
• Robert Mahood — مشرف هندسي
• Andrew Wong (جامعة نيو ساوث ويلز) — مشرف أكاديمي

النسخة النهائية: 13 فبراير 2026