SC4MEC: Automated Implementation of A Secure Hierarchical Calculus for Mobile Edge Computing

Mobile Edge Computing (MEC), as an emerging technology, is proposed to solve the time delay problem in 5G era, especially in the field of autonomous driving. The core idea of MEC is to offload the task to the nearest device/server for computation, i.e., sinking the computation, so as to reduce the delay and congestion. Actually, there are lots of researches on MEC offloading strategy, but there is little research on the computation of its offloading characteristics. Therefore, in this paper, we first propose a secure hierarchical calculus SC4MEC to describe the features of MEC. We also give the syntax and operational semantics of this calculus from the process and network levels, and simulate the calculus in Maude. Meanwhile, local ecology is applied to the communication channel to further reduce the authentication delay of the device with the same identity and ensure the security of the transmission data. We also propose to extend the communication radius of MEC server or cloud server by rule Enlarge, in order to ensure the mobile devices's connectivity while the consumption of resources is minimized. Finally, we employ SC4MEC calculus to a small example about device to device communication with automated implementation.