Process Calculus With Its Formal Semantics,Modeling And Verification Of Mobile Edge Computing

In the 5G era,users are extremely sensitive to time delay and have strict requirements for reliability.The architecture of mobile edge computing(MEC)can effectively reduce or even eliminate the impact of time and network delay.Its core idea is to reasonably localize the data,i.e.,“data sinking”.Actually,most of the current researches still concentrate on how to balance the efficiency and energy consumption of the task offloading strategies of MEC,while few work analyzes and expounds its offloading characteristics from the perspective of formal methods.Therefore,it is a vital research topic to study how to accurately describe its offloading characteristics mathematically,in order to enhance the comprehensive quality of service.In addition,as mobile edge computing adds an edge layer on the basis of cloud computing to offload and process data nearby,it is also of great significance to study the data integrity of its edge layer and the high reliability of the device layer.In this thesis,we are devoted to studying and exploring mobile edge computing from two perspectives of theory and application with different branches of formal methods.In theory,this thesis proposes a hierarchical secure process calculus r MECal for MEC offloading characteristics,and puts forward its relevant operational semantics,denotational semantics,and proof system.Compared with the traditional process calculus,the r MECal calculus fully embodies the hierarchical architecture of mobile edge computing,the offloading characteristics of different data types,security and so on.On the basis of formal semantics,this thesis studies the operational semantics of r MECal calculus,especially designing the parallel combination rules for unicast,multicast and broadcast; Derived from the Unifying Theories of Programming(UTP)proposed by professors C.A.R.Hoare(Turing Award Winner)and Jifeng He,this thesis also studies the denotational semantics of this calculus; Under the guidance of extended Hoare logic,this thesis studies the proof system of r MECal calculus to verify the validity of the program.In application,this thesis makes formal analysis,modeling and verification for the combined protocol AICE of MEC edge layer and the master-salve scheme of MEC device layer.On the basis of SVO logic and tool AVISPA,this thesis formally analyzes and verifies the data integrity of MEC edge layer,and the correctness and security of identity authentication protocol AICE from the perspective of theory and mechanism;with the assistance of timed automata and tool UPPAAL,this thesis formally models and verifies the high reliability of the master-slave scheme design of high-performance switch in MEC device layer.The main contents and contributions of this thesis contain two aspects: theories and applications:Theoretically.(1)This thesis presents a hierarchical secure process calculus r MECal with the offloading feature of mobile edge computing.This calculus proposes three channel types for different security levels,and leads into the concept of “ecosystem” of the same ID(identity)to reduce transmission delay and ensure security.In addition,this calculus not only introduces the layer operator ? and data type characterization to reflect the layer and data offloading characteristics of MEC architecture,but also describes the mobility and resource saving of MEC.(2)This thesis studies the formal semantics of r MECal calculus,including operational semantics,denotational semantics,and proof system.According to the offloading characteristics of four different data types in MEC architecture layer,we propose three priority offloading tables of different data types to fully cover all possible situations,so as to support the design of operational semantics and denotational semantics,so that unicast,multicast and broadcast can be expressed by one rule.Based on Haore logic,we design a proof system of r MECal calculus to verify the correctness of the program.We also show the practicability of this calculus and its proof system through the case of Internet of Vehicles.Practically.(1)This thesis adopts SVO logic and tool AVISPA to formally analyze and verify the correctness and security of AICE protocol in the edge layer of mobile edge computing from the perspective of theoretical analysis and mechanical verification.Aiming at the data integrity of the edge layer of MEC and authentication of users,this thesis gives an integrated protocol AICE,formally analyzes the correctness of the protocol utilizing the SVO logic in modal logic,and verifies the security of this protocol with the tool AVISPA.(2)This thesis employs timed automata and tool UPPAAL to formally model and verify the high reliability of the design of master-slave scheme in the device layer of mobile edge computing.In the light of the demand of high reliability of the device layer in MEC,this thesis proposes to introduce the high-performance switch with master-slave scheme into the D2 D architecture of the device layer,selects timed automata to formally model the master-slave scheme,and then discusses and verifies the properties of master-slave consistency and master-slave synchronization of this scheme respectively,so that the high reliability of this scheme is proved.