Quantitative Analysis and Verification of Edge Computing Offloading Strategy Based on Probabilistic Model Checking

Edge computing has emerged as the leading framework for addressing the need for low latency and high reliability in various applications. To achieve efficient completion of tasks in edge computing, considerable efforts have been made to design effective offloading strategies. However, most of these strategies are proposed without undergoing quantitative analysis and verification to ensure their correctness and robustness. Therefore, this paper presents a hybrid offloading strategy framework, encompassing delay-based, energy-efficient, and energy-delay tradeoff strategies, aimed at improving the comprehensibility and verifiability of offloading strategies, and addressing this gap. Additionally, we employ probabilistic model checking, specifically Prism, to quantitatively analyze and validate the reliability of the proposed hybrid framework. Our method addresses the need for rigorous quantitative analysis and verification of edge computing offloading strategies, ensuring the correctness and robustness. The outcomes of this paper provide practical solutions and insights to the field, advancing the development of trustworthy and efficient offloading strategies for edge computing systems.