David, Alexandre1; Du, DeHui7; Larsen, Kim Guldstrand4; Mikučionis, Marius2; Skou, Arne4
1 Distributed Systems and Semantics, The Technical Faculty of IT and Design, Aalborg University, VBN2 Department of Computer Science, The Technical Faculty of IT and Design, Aalborg University, VBN3 The Faculty of Engineering and Science (TECH), Aalborg University, VBN4 CISS - Center for Embedded Software Systems, The Technical Faculty of IT and Design, Aalborg University, VBN5 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN6 East China Normal University7 East China Normal University
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 .
Science in China. Series F: Information Sciences, 2012, Vol 55, Issue 12, p. 2694-2707