Towards formal verification of smart grids: An effective modelling approach and some first experimentation

Nowadays, smart grids are used widely around the world when they enable detecting, reacting and pro-acting to changes in usage and many concerns with the power system, as well as having self-healing capabilities. Some smart grids have recently been created and operational in Vietnam. To ensure the effectiveness of the smart grids, the correctness of the system designs must be studied carefully before the explosion of the use of smart grids, particularly in developing countries such as Vietnam. As formal methods, including formal verification and model checking, recently play more important role in verifying smart grid properties such as load balancing and fault resilience, the effectiveness of formal verification depends mostly on system modeling and verification techniques. Recent researches have shown the feasibility of applying model-checking tools in smart grid verification, and also the inability to test complex properties and systems. In our opinion, the inability could be come from the complicating of the models of the system-under-test. In this study, we suggested a new method for representing smart grids using Colored Petri Net (CPN), a formal representa- tion language. In comparing to the current modeling approach, the new model allows engineers transforms complex grids into simple models. Moreover, based on the advantages of the “color” aspect of the CPN, the result model can be easily upgraded to adapt to the changes of the original smart grids without re- modeling. Also in this study, a basic case study for representing a smart grid, which consists of multiple power sources and multiple consumers, will be shown. The model will be configured to capture some problems that may happen in the grid such as the changing of the capacity of the power sources. The verification experimentation conducted on the case study shows the usefulness of the proposed method.