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.

翻译：基于IEEE 802.15.4的电网自组织传感器网络大规模部署带来了可靠性挑战，即当节点为最大化个体性能而自私地调整CSMA/CA参数时，此类行为会降低可靠性、能效及对严格电网约束的遵从性。现有解析与仿真方法往往难以在异步、事件驱动及资源受限条件下严格评估配置方案。本文开发了一种验证框架，该框架将随机定时混合自动机与带置信边界的统计模型检验（SMC）相结合，以形式化评估电网工作负载下的CSMA/CA参数化配置。通过用时序逻辑编码节点级与系统级目标，并借助大规模统计评估实现协议筛选自动化，本方法可认证对单方偏离保持稳健的纳什均衡策略。在变电站规模场景中，相较于激进调优基线，经认证的均衡策略将效用从0.862提升至0.914，并将投递率从89.5%提高至93.2%。相较于面向投递的基线策略，其在保持相当投递性能的同时，将每周期平均能耗从152.8 mJ降低至149.2 mJ。经认证的配置方案在满足时延、可靠性与能耗约束的同时，其稳健系数高于0.97，效用值超过0.91。