Quantitative Analysis and Verification of Edge Computing Offloading
Strategy Based on Probabilistic Model Checking
Abstract
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.
