Search

Modern cyber-physical microgrids rely on the information exchanged among power electronics devices (i.e., converters or inverters with local embedded controllers) making them vulnerable to cyber manipulations. The physical devices themselves are susceptible to potential faults and failures. Effects of these cyber and physical anomalies can propagate throughout the entire microgrid due to information exchanged and the inherent low inertia of the distribution network. This work employs the parametric time-frequency logic (PTFL) framework to detect such cyber-physical anomalies. PTFL is a formalism to analyze the time-frequency content of the observable quantities of interest (such as current, voltage, or frequency) of power electronics devices in comparison with the predefined time-frequency properties. PTFL formalism is presented to detect the anomalies such as false data-injection attacks, denial-of-service attacks, and faults on a cluster of four DC microgrids and an inverter-populated IEEE 34-bus feeder system in a controller/hardware-in-the-loop environment.

An explainable intelligent framework for cyber anomaly mitigation of cyber-physical inverter-based systems is presented.Smart inverter-based microgrids essentially constitute an extensive communication layer that makes them vulnerable to cyber anomalies. The distributed cooperative controllers implemented at the secondary control level of such systems exchange information among physical nodes using the cyber layer to meet the control objectives. The cyber anomalies targeting the communication network may distort the normal operation therefore, an effective cyber anomaly mitigation technique using an artificial neural network (ANN) is proposed in this paper. The intelligent anomaly mitigation control is modeled using adynamic recurrent neural network that employs a nonlinear autoregressive network with exogenous inputs. The effects of false data injection to the distributed cooperative controller at the secondary control level are considered. The training data for designing the neural network are generated by multiple simulations of the designed microgrid under various operating conditions using MATLAB/Simulink. The neural network is trained offline and tested online in the simulated microgrid. The proposed technique is applied as secondary voltage and frequency control of distributed cooperative control-based microgrid to regulate the voltage under various operating conditions. The performance of the proposed control technique is verified by injecting various types of false data injection-based cyber anomalies. The proposed ANN-based secondary controller maintained the normal operation of microgrid in the presence of cyber anomalies as demonstrated by real-time simulations on a real-time digital simulator OPAL-RT.

Emerging converter-dominated dc microgrids employ distributed cooperative control strategies and communication network. Since there is no central entity to monitor and assess the global cyber scenario, microgrids employing distributed control are prone to cyber attacks. This work presents signal temporal logic (STL) detection of two major types of cyber attacks, namely false-data injection attacks and denial-of-service attacks. Such cyber attacks can compromise voltage regulation and load sharing in dc microgrids. STL is a formalism to monitor the output voltages and currents of dc microgrids against the defined specifications, such as operational bounds, over time. Besides detection, the proposed approach also quantifies the attack impact. Moreover, it can be effectively employed for a complex dc microgrid without prior knowledge of its dynamics. This detection technique is successfully demonstrated using a physical microgrid setup or in a hardware-in-the-loop environment, where various attacks are formalized, detected, and quantified.

The distributed cooperative controllers for inverter-based systems rely on communication networks that make them vulnerable to cyber anomalies. In addition, the distortion effects of such anomalies may also propagate throughout inverter-based cyber-physical systems due to the cooperative cyber layer. In this paper, an intelligent anomaly mitigation technique for such systems is presented utilizing data driven artificial intelligence tools that employ artificial neural networks. The proposed technique is implemented in secondary voltage control of distributed cooperative control-based microgrid, and results are validated by comparison with existing distributed secondary control and real-time simulations on real-time simulator OPAL-RT., Accepted at: 2021 IEEE Energy Conversion Congress and Exposition (ECCE)

This work adopts an online resiliency monitoring framework employing metric temporal logic (MTL) under cyber-physical anomalies, namely false-data injection attacks, denial-of-service attacks, and physical faults. Such anomalies adversely affect the frequency synchronization, load sharing, and voltage regulation in microgrids. MTL formalism is adopted to monitor the outputs of inverters/converters against operational bounds, detect and quantify cyber-physical anomalies, monitor the microgrid’s resiliency during runtime, and compare mitigation strategies. Since the proposed framework does not require system knowledge, it can be deployed on a complex microgrid. This is verified using an IEEE 34-bus feeder system and a DC microgrid cluster in a controller/hardware-in-the-loop environment.

Power electronics-intensive dc microgrids use increasingly complex software-based controllers and communication networks. They are evolving into cyber-physical systems (CPS) with sophisticated interactions between physical and computational processes, making them vulnerable to cyber attacks. This paper presents a framework to detect possible false-data injection attacks (FDIAs) in cyber-physical dc microgrids. The detection problem is formalized as identifying a change in sets of inferred candidate invariants. Invariants are microgrids properties that do not change over time. Both the physical plant and the software controller of CPS can be described as Simulink/Stateflow (SLSF) diagrams. The dynamic analysis infers the candidate invariants over the input/output variables of SLSF components. The reachability analysis generates the sets of reachable states (reach sets) for the CPS modeled as hybrid automata. The candidate invariants that contain the reach sets are called the actual invariants. The candidate invariants are then compared with the actual invariants, and any mismatch indicates the presence of FDIA. To evaluate the proposed methodology, the hybrid automaton of a dc microgrid, with a distributed cooperative control scheme, is presented. The reachability analysis is performed to obtain the reach sets and, hence, the actual invariants. Moreover, a prototype tool, HYbrid iNvariant GEneratoR, is extended to instrument SLSF models, obtain candidate invariants, and identify FDIA.

This paper presents hybrid automaton modeling, comparative model validation, and formal verification of stability through reachability analysis of pulse width modulation (PWM) dc–dc converters. Conformance degree provides a measure of closeness between the proposed hybrid automata models and experimental data. Nondeterminism due to variations in circuit parameters is modeled using interval matrices. In direct contrast to the unsound and computationally-intensive Monte Carlo simulation, reachability analysis is introduced to overapproximate the set of reachable states and ensure stable operation of PWM dc–dc converters. Using a 200 W experimental prototype of a buck converter, hybrid automata models of open-loop, and hysteresis-controlled converters are first validated against experimental data using their conformance degrees. Next, converter stability is formally verified through reachability analysis and informally validated using Monte Carlo simulations and experimental results.

Hybrid automata are an important formalism for modeling dynamical systems exhibiting mixed discrete–continuous behavior such as control systems and are amenable to formal verification. However, hybrid automata lack expressiveness compared to integrated model-based design frameworks such as the MathWorks’ Simulink/Stateflow (SlSf). In this paper, we propose a technique for correct-by-construction compositional design of cyber-physical systems (CPS) by embedding hybrid automata into SlSf models. Hybrid automata are first verified using verification tools such as SpaceEx and then automatically translated to embed the hybrid automata into SlSf models such that the properties verified are transferred and maintained in the translated SlSf model. The resultant SlSf model can then be used for automatic code generation and deployment to hardware, resulting in an implementation. The approach is implemented in a software tool building on the HyST model transformation tool for hybrid systems. We show the effectiveness of our approach on a CPS case study—a closed-loop buck converter—and validate the overall correct-by-construction methodology: from formal verification to implementation in hardware controlling an actual physical plant.

Various mission-critical applications necessarily require a transformer in switching converters to obtain DC isolation between the converters’ input and output. Since DC-DC converters are the switching devices, these are modeled as hybrid automata. We present hybrid automaton modeling of two main types of transformer isolated DC-DC converters, namely, flyback and forward converters. We have also catered the non-determinism for both. We use HyST (Hybrid Source Transformation) tool to automatically generate the models in SpaceEx format, perform reachability analysis, and then automatically convert the models into Mathworks Simulink Stateflow (SLSF) using HyST. Thus we demonstrate effectiveness of HyST tool in the model-based design process. The HyST user needs not to manually construct or modify the models thus saving significant amount of time and efforts.

Analog-mixed signal (AMS) circuits are widely used in various mission-critical applications necessitating their formal verification prior to implementation. We consider modeling two AMS circuits as hybrid automata, particularly a charge pump phase-locked loop (CP-PLL) and a full-wave rectifier (FWR). We present executable models for the benchmarks in SpaceEx format, perform reachability analysis, and demonstrate their automatic conversion to MathWorks Simulink/Stateflow (SLSF) format using the HyST tool. Moreover, as a next step towards implementation, we present the VHDL-AMS description of a circuit based on the verified model.