<p>Cascading failures in Wireless Sensor Networks (WSNs) exhibit dynamic spatial-temporal evolution, propagating from local disruptions to global network collapse. Identifying the spatial-temporal features of cascading failures in WSNs can provide critical support for network planning and adjustment, and is essential for ensuring normal operation and enhancing network robustness. Existing approaches suffer from limited modeling expressiveness, lack of causal reasoning, and weak verifiability, making them insufficient to support the regulation and defense of WSNs. To address these limitations, we propose a novel approach based on spatial-temporal model checking to identify the spatial-temporal features of cascading failures in WSNs. However, the closure space model for spatial reasoning and the Spatial-Temporal Logic for Closure Space (STLCS) for formal specification have limitations in reasoning about and describing the spatial-temporal features of cascading failures in WSNs. To better integrate model checking into our framework, we first extend the closure space model and STLCS logic to capture dynamic node properties and enhance the expressiveness for complex spatial-temporal behaviors. Then, we construct a formal spatial-temporal model of the WSN, define spatial-temporal logic formulas, and finally perform verification. Experimental results demonstrate that our method enables automated, logical and comprehensive identification of the features of cascading failures in WSNs.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Model checking spatial-temporal features of cascading failures in wireless sensor networks

  • Junjie Li,
  • Jun Niu

摘要

Cascading failures in Wireless Sensor Networks (WSNs) exhibit dynamic spatial-temporal evolution, propagating from local disruptions to global network collapse. Identifying the spatial-temporal features of cascading failures in WSNs can provide critical support for network planning and adjustment, and is essential for ensuring normal operation and enhancing network robustness. Existing approaches suffer from limited modeling expressiveness, lack of causal reasoning, and weak verifiability, making them insufficient to support the regulation and defense of WSNs. To address these limitations, we propose a novel approach based on spatial-temporal model checking to identify the spatial-temporal features of cascading failures in WSNs. However, the closure space model for spatial reasoning and the Spatial-Temporal Logic for Closure Space (STLCS) for formal specification have limitations in reasoning about and describing the spatial-temporal features of cascading failures in WSNs. To better integrate model checking into our framework, we first extend the closure space model and STLCS logic to capture dynamic node properties and enhance the expressiveness for complex spatial-temporal behaviors. Then, we construct a formal spatial-temporal model of the WSN, define spatial-temporal logic formulas, and finally perform verification. Experimental results demonstrate that our method enables automated, logical and comprehensive identification of the features of cascading failures in WSNs.