Quantitative modelling and analysis of a Chinese smart grid: a stochastic model checking case study

Cyber-physical systems integrate information and communication technology with the physical elements of a system, mainly for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. One of the important issues in this context is the verification of certain quantitative properties of the system. In this paper, we consider a specific Chinese smart grid implementation as a case study and address the verification problem for performance and energy consumption. We employ stochastic model checking approach and present our modelling and analysis study using PRISM model checker.