Verification of Networks of Smart Energy Systems over the Cloud
详细信息 查看全文
- 关键词：Cyber ; physical systems ; Systems of systems ; Internet of things ; Hybrid models ; Stochastic processes ; Nondeterminism ; Partial observations ; Real ; time systems ; Security ; Model learning ; (quantitative) probabilistic verification ; Formal abstractions ; Bisimulations ; Statistical verification ; Feedback controllers ; Policy and strategy synthesis ; Distributed control ; Safety and performance ; Games ; Correct ; by design synthesis ; Autonomy ; Energy and power networks ; Electricity demand ; response ; Thermostatically controlled loads
- 刊名：Lecture Notes in Computer Science
- 出版年：2017
- 出版时间：2017
- 年：2017
- 卷：10152
- 期：1
- 页码：1-14
- 丛书名：Numerical Software Verification
- ISBN：978-3-319-54292-8
- 卷排序：10152
文摘
This contribution advocates the use of formal methods to verify and certifiably control the behaviour of computational devices interacting over a shared infrastructure. Formal techniques can provide compelling solutions not only when safety-critical goals are the target, but also to tackle verification and synthesis problems on populations of such devices: we argue that alternative solutions based on classical analytical techniques or on approximate computations are prone to errors with global repercussions, and instead propose an approach based on formal abstractions, error-based refinements, and the use of interface functions for the synthesis of abstract controllers and their concrete implementation. Two applicative areas are elucidated, dealing respectively with thermal loads and electricity-generating devices interacting over a smart energy network or over a local power grid. We discuss the aggregation of large populations of thermostatically-controlled loads and of photovoltaic panels, and the corresponding problems of energy management in smart buildings, of demand-response on smart grids, and respectively of frequency stabilisation and grid robustness.