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

Edge computing has become a key framework for meeting the demands of low latency and high reliability across various applications. To ensure efficient task execution in edge computing, many offloading strategies have been proposed; however, most lack quantitative analysis and formal verification to guarantee their correctness. This paper addresses this gap by presenting an integrated offloading strategy that combines delay-based, energy-efficient, and energy-delay trade-off approaches, enhancing both the clarity and verifiability of offloading methods. Furthermore, we apply probabilistic model checking using PRISM to rigorously analyze and validate the correctness of the proposed hybrid strategy. Our approach provides practical solutions and valuable insights, promoting the development of reliable and efficient offloading strategies for edge computing systems.