Formal evaluation of scheduling strategies for smart building air-conditioning systems under uncertain environment

In recent years people have witnessed an increased worldwide attention to the concept of smart buildings. Compared with traditional counterpart, smart buildings are more energy efficient, comfortable and maintainable. Hence, smart buildings are becoming the mainstream of future building construction. As a key part of smart building ventilation systems, air conditioners highly impact the overall energy consumption of smart buildings as well as the experience of their occupants. Therefore, how to design and evaluate feasible scheduling strategies of air conditioning systems becomes a major challenge in the design of smart buildings. Especially when many uncertain factors caused by physical environment are involved, the complexity of strategy evaluation increases drastically. Although existing approaches allow the evaluation of smart buildings from the perspectives of energy consumption and performance, few of them consider the evaluation of the scheduling strategies themselves. Based on priced timed automata, this paper proposes an efficient framework that enables accurate modeling and evaluation of scheduling strategies of smart building air-conditioning systems with uncertain environment. This framework utilizes the statistical model checker UPPAAL-SMC as the engine to quantitatively analyze user-specified performance queries in the form of properties. Based on the underlying random simulation runs monitored by UPPAAL-SMC, the framework can automatically report the quantitative analysis results of energy consumption and user satisfaction under uncertain environment. Experimental results show that the proposed approach can effectively help smart building designers to make their decisions in the selection and optimization of scheduling strategies.