Formal Verification of HPS-based Master-Slave Scheme in MEC with Timed Automata

The combination of D2D (Device to Device) communication and MEC (Mobile Edge Computing) architecture is adopted to reduce the communication delay in 5G. With the extensive use of HPS (high performance switch) as the main medium of data distribution in the device layer, the holistic power consumption and delay can be guaranteed stably, mainly because HPS has the mechanism of Master-Slave scheme to ensure the robustness. However, as far as we know, there are fewer studies to verify the safety validation of the design using formal methods. Hence, we study it through timed automata and model checking. This paper integrates HPS into D2D communication design in MEC, selects the Master-Slave synchronization and switchover scheme in HPS as the research object, describes the scheme based on timed automata, and then verifies seven fundamental but essential properties through the model checker UPPAAL. Through verification, comparison and analysis of possible scenarios in our constructed model, it can be concluded that the design of the HPS in MEC can conform to its required specification. Further, it can not only enhance the safety validation of the combination of D2D communication and MEC architecture, but also provide a guide for the newest subsequent high safety primary-backup design in industry.