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

TL;DR

This paper presents a formal verification framework using statistical model checking to optimize CSMA/CA parameters in power-grid sensor networks, ensuring reliability, efficiency, and adherence to grid constraints.

Contribution

It introduces a novel verification approach combining stochastic hybrid automata and SMC to certify robust, equilibrium-based CSMA/CA configurations for power-grid sensor networks.

Findings

Certified equilibrium strategies improve utility and delivery ratio.

Energy consumption is reduced while maintaining delivery performance.

Configurations meet latency, reliability, and energy constraints with high robustness.

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.