View article

Energy router (ER) based system is a crucial part of the energy transmission and management under the circumstance of energy Internet for green cities. During its design process, a sound formal verification and a performance monitoring scheme are needed to check its reliability and meaningful quantitative properties. In this paper, we provide formal verification solutions for an ER-based system by proposing a continuous-time Markov chain model describing the architecture of the ER-based system. To verify real-world function of the ER-based system, we choose electricity trading to propose a Markov decision process model based on an ER subsystem to describe the trading behavior. To monitor the system performance, we project the energy scheduling process in the ER-based system, and then implement this scheduling process on top of a cloud computing experiment tool. Finally, we perform extensive …