Engineering

Reliability engineering

Statistics

Markov process

Embedded system

Real-time computing

Theoretical computer science

Probabilistic logic

Energy (signal processing)

Scheduling (production processes)

Operating system

The Internet

Computer science

Cloud computing

Markov decision process

Distributed computing

Computer network

Mathematics

Operations management

Artificial intelligence

Router

Model checking

IEEE Transactions on Industrial Informatics

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 experiment evaluations to investigate the system reliability properties, quantitative properties, and scheduling behaviors. The experiment verifies the effectiveness of the proposed models and the monitoring scheme.

Probabilistic Model Checking and Scheduling Implementation of an Energy Router System in Energy Internet for Green Cities