不确定环境下智能大厦空调系统调度策略评估

近年来,智能大厦的概念在国内外受到了高度的关注.相比于传统的建筑,智能大厦更加节能、舒适、易维护,已成为未来建筑的发展趋势.作为智能大厦空调通风系统的关键部分,空调系统及其调度策略决定了大厦整体的节能效果以及大厦中用户的舒适度.然而由于智能大厦所处的环境具有许多不确定因素,这极大增加了空调系统调度策略设计与评估的复杂程度.因此如何设计与评估不确定环境下空调系统的调度策略成为了智能大厦设计者面临的一大挑战.已有的方法主要针对智能大厦空调系统进行能耗与性能等方面的分析,但尚未有方法针对调度策略本身进行分析与评估.提出了一种基于价格时间自动机的调度策略评估框架,支持对不确定环境下的智能大厦进行精确建模与定量评估.该框架使用UPPAAL-SMC作为属性查询引擎对模型进行随机模拟运行,根据模拟结果对不同调度策略下大厦的能耗及用户的舒适度进行定量分析.实验结果表明,该方法能有效地帮助设计者进行策略的制定和选取.

Formal Evaluation of Scheduling Strategies for Smart Building Air-Conditioning Systems under Uncertain Environment

In recent years people have witnessed an increasing worldwide concern about the concept of smart buildings. Compared with traditional counterpart, smart buildings are more energy-efficient, comfortable and easy-maintainable. Hence, smart buildings are becoming the mainstream of future building construction. As a key part of smart building ventilation systems, air-conditioners strongly determine the overall energy consumption of smart buildings as well as the experience of their occupants. Therefore, how to design and evaluate all feasible scheduling strategies of air-conditioning systems is becoming 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 will increase drastically. Although existing approaches allow the evaluation of smart buildings from the perspectives of energy consumption, performance, etc., few of them consider the evaluation of the scheduling strategies themselves. Based on the priced timed automata, this paper proposes an efficient framework that enables the accurate modeling and evaluation of scheduling strategies of smart building air-conditioning systems with uncertain environment. Our framework utilizes the statistical model checker UPPAAL-SMC as the engines to quantitatively analyze user-specified performance queries in the form of properties. Based on the underlying random simulation runs monitored by UPPAAL-SMC, our framework can automatically report the quantitative analysis results of energy consumption and user satisfaction under uncertain environment. Experimental results show that our approach can effectively help smart building designers to make their decisions in the selection and optimization of scheduling strategies.