The Operational and Denotational Semantics of rMECal Calculus for Mobile Edge Computing

In the era of 5G, users are extremely sensitive to time delay and have strict reliability requirements. The architecture of MEC can effectively reduce or even eliminate the impact of return delay, whose core idea is to localize the data reasonably. Actually, most of the work still concentrated on the balance between the efficiency and energy consumption of task offloading strategy, but few work analyzed and expounded its offloading characteristics from the perspective of formal methods. Henceforth, In this paper, we propose a real-time secure hierarchical process calculus rMECal of task offloading for MEC. Then we show the operational semantics of this calculus from the process and network levels to describe how the program works, especially the parallel composition rule for many-to-many broadcast communication. In addition, we formalize the calculus and rules with real-time Maude, and adopt the example of Internet of Vehicles to illustrate the availability of the calculus and operational semantics. Moreover, we give the denotational semantics of this calculus to express what the program executes based on the Unifying Theories of Programming (UTP) approach, and show the fundamental algebraic properties. We believe that this paper can provide a guidance for exploring the formal theories in MEC.