Parallel Statistical Model Checking for Safety Verification in Smart Grids
By using small computing devices deployed at user premises, Autonomous Demand Response (ADR) adapts users electricity consumption to given time-dependent electricity tariffs. This allows end-users to save on their electricity bill and Distribution System Operators to optimise (through suitable time-dependent tariffs) management of the electric grid by avoiding demand peaks. Unfortunately, even with ADR, users power consumption may deviate from the expected (minimum cost) one, e.g., because ADR devices fail to correctly forecast energy needs at user premises. As a result, the aggregated power demand may present undesirable peaks. In this paper we address such a problem by presenting methods and a software tool (APD-Analyser) implementing them, enabling Distribution System Operators to effectively verify that a given time-dependent electricity tariff achieves the desired goals even when end-users deviate from their expected behaviour. We show feasibility of the proposed approach through a realistic scenario from a medium voltage Danish distribution network.
Code (0)
등록된 구현이 없습니다.
Tasks
ManagementSimilar Papers 제목 키워드 기반
Safeguarding Learning-based Control for Smart Energy Systems with Sampling Specifications
We study challenges using reinforcement learning in controlling energy systems, where apart from performance requirements, one has additional safety requirements such as avoiding blackouts. We detail how these safety req…
reinforcement-learningReinforcement LearningSafe Reinforcement LearningIncremental Bounded Model Checking of Artificial Neural Networks in CUDA
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for…
GPUStateless and Rule-Based Verification For Compliance Checking Applications
Underlying computational model has an important role in any computation. The state and transition (such as in automata) and rule and value (such as in Lisp and logic programming) are two comparable and counterpart comput…
Formal LogicBDD for Complete Characterization of a Safety Violation in Linear Systems with Inputs
The control design tools for linear systems typically involves pole placement and computing Lyapunov functions which are useful for ensuring stability. But given higher requirements on control design, a designer is expec…
Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-…