Abstract: The embedded terminals in the power grid cyber physical systems need to not only have the ability of information interaction, but also meet the real-time requirements of measurement and control under resource constraints. It is necessary to introduce formal methods to verify the reliability of complex systems with large scale. This paper analyzes the application of formal methods in power grid cyber physical systems, designs and realizes a formal method and model checking software tool for analyzing the information interaction process of embedded system in the power grid cyber physical systems. The application process of the model checking tool is analyzed in detail through a practical case, and the application results show that the formal method can shorten the distance from high level design to code implementation and improve the reliability of the products. The model checking software tool can provide a reference solution to the reliability assurance problem caused by the rapid increase of embedded devices in terms of scale and complexity.