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 for-
malisms 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 modeling 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 behaviour, ...). To demonstrate the intended use and usefulness of our framework, we present an
application to the Hybrid Systems Verification Benchmark of [10].