A Formal Approach to Testing Logical Reliablity of Intelligent Device in Home Energy Management System

Home energy management system (HEMS), which typically consists of a gateway, several smart plugs and other intelligent devices, plays an increasingly significant role in smart grid. Due to sophisticated functions and complex underlying software designing of the intelligent devices, it has become increasingly challenging to critically verify their reliability. This paper demonstrates that the formal methodology can be equally applied to software designs of those intelligent devices in HEMS. In this paper, timed automaton (TA) is adopted to describe the formal specifications of intelligent devices and UPPAAL, which is based on timed computation tree logic (TCTL), is applied as the model checker to execute formal verifications of the above formal specifications. Then, abnormal protections of smart plug such as overcurrent protection, overvoltage protection and under-voltage protection are taken as examples to show how UPPAAL can be implemented to present the formal specifications and formal verifications of the software designing of the intelligent devices in HEMS. This same technique is universal to a wide variety of software designs in smart grid, and the information it provides is invaluable as a necessary and useful supplement of simulation to software engineers during the development of new systems.