An evaluation framework for energy aware buildings using statistical model checking

Cyber-physical systems are to be found in numerous applications throughout society. The principal barrier to develop trustworthy cyber-physical systems is the lack of expressive modelling and specification formalisms supported by efficient tools and methodologies. To overcome this barrier, we extend in this paper the modelling formalism of the tool UPPAAL-SMC to stochastic hybrid automata, thus providing the expressive power required for modelling complex cyber-physical systems. The application of Statistical Model Checking provides a highly scalable technique for analyzing performance properties of this formalisms. A particular kind of cyber-physical systems are Smart Grids which together with Intelligent, Energy Aware Buildings will play a major role in achieving an energy efficient society of the future. In this paper we present a framework in UPPAAL-SMC for energy aware buildings allowing to evaluate the performance of proposed control strategies in terms of their induced comfort and energy profiles under varying environmental settings (e.g. weather, user behavior etc.). To demonstrate the intended use and usefulness of our framework, we present an application to the Hybrid Systems Verification Benchmark.