Statistical Verification of Medium-Access Parameterization for Power-Grid Edge Ad Hoc Sensor Networks

TL;DR

This paper addresses reliability and efficiency challenges caused by selfish adaptation of IEEE 802.15.4 CSMA/CA parameters in power-grid edge sensor networks. It proposes a verification pipeline that combines stochastic timed hybrid automata (STHA) with statistical model checking (SMC) to quantify utilities under grid workloads and certify grid-constrained Nash equilibria via a two-stage screening and certification process. Key contributions include a CBTL specification framework for node and network objectives, a $\Delta$-relaxed Nash equilibrium notion, and empirical evidence that certified configurations meet latency, reliability, and energy constraints with high robustness (e.g., $\Delta_{grid}$ and utilities above $0.91$). In a substation-scale scenario, certified equilibria improve utility from $0.862$ to $0.914$ and delivery ratio from $89.5\%$ to $93.2\%$, while reducing mean energy per cycle from $152.8\ \mathrm{mJ}$ to $149.2\ \mathrm{mJ}$. The framework offers a scalable, formal guarantee mechanism for grid operators to screen and deploy parameterizations that resist unilateral deviations under regulatory constraints.

Abstract

The widespread deployment of power grid ad hoc sensor networks based on IEEE 802.15.4 raises reliability challenges when nodes selfishly adapt CSMA/CA parameters to maximize individual performance. Such behavior degrades reliability, energy efficiency, and compliance with strict grid constraints. Existing analytical and simulation approaches often fail to rigorously evaluate configurations under asynchronous, event-driven, and resource-limited conditions. We develop a verification framework that integrates stochastic timed hybrid automata with statistical model checking (SMC) with confidence bounds to formally assess CSMA/CA parameterizations under grid workloads. By encoding node- and system-level objectives in temporal logic and automating protocol screening via large-scale statistical evaluation, the method certifies Nash equilibrium strategies that remain robust to unilateral deviations. In a substation-scale scenario, the certified equilibrium improves utility from 0.862 to 0.914 and raises the delivery ratio from 89.5% to 93.2% when compared with an aggressive tuning baseline. Against a delivery-oriented baseline, it reduces mean per-cycle energy from 152.8 mJ to 149.2 mJ while maintaining comparable delivery performance. Certified configurations satisfy latency, reliability, and energy constraints with robustness coefficients above 0.97 and utility above 0.91.

Figures (1)

• Figure 1: UPPAAL timed automata model of a sensor node implementing the IEEE 802.15.4 CSMA/CA protocol, parameterized for power grid IoT scenarios. The model captures the full protocol state space, including channel contention, backoff, retransmission, and per-state energy accounting, and serves as the core simulation engine for all experimental evaluation and statistical screening in this study.