## 1 Introduction  
The cyber physical system (CPS) refers to the next generation of engineering systems. It requires tight integration of computation, communication, and control technologies to achieve stability, reliability, and expandability, and has been applied in many application domains such as transportation, health care and energy [1]. With the deep and pervasive application of information and communication technologies, smart grid has become one of the vital CPSs [2]. To improve the safety and efficiency of smart grid, the user energy management system (UEMS) plays an increasingly crucial role in serving as an agent of consumers to respond to demand response signals, i.e., automated demand response (ADR) [3]. Many previous works related to the UEMS in ADR programs focus on energy management strategies or algorithms. [PERSON] et al. developed a demand response strategy with the application of machine learning and optimization scheduling [4]. [PERSON] et al. formulated a fully automated EMS rescheduling problem as a reinforcement learning problem [5]. [PERSON] et al. applied partially observable Markov decision process approaches in home energy management system (HEMS) for minimizing the household electricity bills in the real-time pricing market [6]. [PERSON] et al. compares an in-home energy management application with an optimization-based residential energy management scheme in the aspect of energy saving and peak load shift under the presence of local energy generation capability, prioritized appliances, and for real-time pricing [7]. Cyber systems such as communication networks and computing modules are indispensable for those strategies or algorithms. However, the cyber systems are always assumed to be ideal in these literatures. In other words, these algorithms may lose efficacy in real projects due to the interdependence and interplay between the cyber system and physical system [8]. For instance, unreliable communication cannot conduct commands exactly, so it may deteriorate the performance of algorithm. To reduce the risks and to develop methods for improving system efficiency, the cyber-physical characteristics of the UEMS should be studied. Besides the communication reliability, as a networked control system composed by intelligent electronic devices, a UEMS must accomplish some logical verification to achieve reliable control. Although the formal methodology is one of the critical methods in CPS analyses and can ensure the system robustness from the aspect of logic, there are rare researches related to the formal methodology analyzing the reliability of the UEMS in ADR. The formal-methodology-based cyber-physical analyses mainly focus on distribution networks, such as intelligent substations based on IEC61850 [9; 10; 11] or microgrids [12; 13]. The manuscript could be divided into three parts: the optimization problem of the UEMS, the basic behaviors of intelligent terminal in UEMS, and the cyber-physical interplay analyses. The optimization problem is to achieve the optimal operation of the physical system and it provides a problem scenario, i.e., optimal operation strategies for multiple electrical heaters in this paper. The basic behaviors aim to establish formal specifications and verifications of the cyber system and to present a way of cyber-physical interplay. The two parts mentioned above are both preparation work for the last cyber-physical interplay analyses. The contributions and innovations of this paper are as follows:  
1. The interdependence and interplay between the cyber system and the physical system of the UEMS is analyzed and the impact of communication reliability on the ADR performance is studied. 2. The major behaviors of intelligent devices in the UEMS are summarized and the corresponding basic MQTT/MQTT-SN topics for the UEMS are proposed. Some modifications are made on original MQTT/MQTT-SN for convenience and high efficiency. For example, the subscription or registration of those topics is added into the connection procedures. 3.