Idea 5: Verified Safe Neural Control for ESP32 in Closed-Loop Systems
Overview
Build a safety-verified neural controller on ESP32 for a physical system (inverted pendulum, DC motor, or power factor correction). Implement on-device formal verification using interval arithmetic to prove that for all bounded sensor noise and disturbances, the controller output stays within safe actuator limits.
Research Gap
- Existing NN-based control on ESP32 (e.g., smart grid power factor correction) provides no safety guarantees
- Neural networks can output dangerous control actions due to adversarial inputs or distribution shift
- Formal verification of NNs exists (Reluplex, Marabou) but requires GPU/cloud and cannot run on MCUs
- No prior work demonstrates runtime neural network verification on a microcontroller
Key Innovation
First TinyML system with runtime neural network verification on a microcontroller. Use lightweight interval arithmetic or zonotope propagation to provide safety guarantees with bounded computational overhead.
Hardware Requirements
| Component | Specification | Purpose |
|---|---|---|
| Main MCU | ESP32-S3-DevKitC | Compute and control platform |
| Plant | DC motor + encoder, or inverted pendulum kit | Controlled physical system |
| Driver | L298N or DRV8833 motor driver | Actuator interface |
| Sensor | Encoder, IMU, or current sensor | State feedback |
| Safety | Emergency stop button, current limiter | Physical safety backup |
Technical Approach
Phase 1: Plant and Baseline Controller
- Identify plant dynamics (e.g., DC motor: Jdω/dt + bω = K*I)
- Design a PID controller as baseline and safety backup
- Verify PID stability using standard control theory
- Establish performance metrics: settling time, overshoot, steady-state error
Phase 2: Neural Network Controller
- Train a small MLP (2-3 hidden layers, 16-64 neurons each) to mimic or exceed PID performance
- Use imitation learning from PID or reinforcement learning in simulation
- Quantize to INT8; deploy on ESP32
- Verify performance matches or exceeds PID in nominal conditions
Phase 3: On-Device Verification Engine
-
Interval Arithmetic Approach:
- For each layer, propagate input intervals [x_low, x_high] through weights and activations
- Output: interval [u_low, u_high] for control action
- If [u_low, u_high] ⊆ [u_min, u_max] (safe actuator limits), accept NN output
- Else, fall back to PID controller
-
Zonotope Approach (more precise):
- Represent uncertainty as zonotopes (affine sets)
- Propagate through network using affine transformations
- Tighter bounds than interval arithmetic, but more computation
Phase 4: Implementation
- Verification runs in parallel with inference (or immediately after)
- Worst-case verification time must be < control period (e.g., 10 ms)
- If verification fails, use PID output and log the event
- Maintain statistics: verification pass rate, fallback rate
Phase 5: Safety Under Adversarial/Noisy Conditions
- Inject sensor noise (Gaussian, uniform, bounded)
- Inject adversarial perturbations (FGSM, PGD adapted for control)
- Show that verified system never violates actuator limits
- Compare against unverified NN (which will violate limits under attack)
Expected Results
- 100% safety guarantee for bounded noise (provable)
- NN controller used >90% of time in nominal conditions
- Verification overhead <20% of control period
- Demonstration on real hardware with injected faults
- Formal proof of safety for the verification algorithm
Target Venues
- IEEE Transactions on Automatic Control (TAC)
- ACM Transactions on Embedded Computing Systems (TECS)
- IEEE Real-Time Systems Symposium (RTSS)
- ACM EMSOFT
Related Work to Cite
- Katz et al., “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks” (CAV 2017)
- Ivanov et al., “Verisig: verifying safety properties of hybrid systems with neural network controllers”
- Neural network control papers (e.g., NN-based MPC, reinforcement learning control)
- Interval arithmetic and reachability analysis (e.g., CORA toolbox)
- ESP32 control applications (power factor correction, motor control)
Risk Mitigation
| Risk | Mitigation |
|---|---|
| Verification too slow | Use very small network; precompute partial results; use INT8-only arithmetic |
| Bounds too conservative (always fallback) | Use zonotopes or symbolic propagation for tighter bounds |
| Real plant unstable | Start with simulated plant (Simulink/MATLAB); then migrate to hardware |
| Adversarial attacks too strong | Focus on bounded noise; adversarial robustness is secondary |
Timeline (Approximate)
- Weeks 1-2: Plant setup, PID controller design and tuning
- Weeks 3-4: Neural network controller training and quantization
- Weeks 5-6: Interval arithmetic verification engine in C
- Weeks 7-8: Integration with real-time control loop
- Weeks 9-10: Safety evaluation with noise/fault injection and paper writing