Graduation Semester and Year
2017
Language
English
Document Type
Dissertation
Degree Name
Doctor of Philosophy in Electrical Engineering
Department
Electrical Engineering
First Advisor
Ali Davoudi
Second Advisor
Taylor Johnson
Abstract
Power electronics-intensive DC distribution networks are emerging as popular alternative to their AC counterparts being more efficient and reliable power delivery platforms. With the recent evolution of control methodology from legacy centralized architecture to distributed control strategy employing communication networks, the DC distribution networks employing such software-based control schemes are evolving into cyber-physical systems. Since there is no central entity to monitor and assess the global cyber scenario, such cyber-physical systems are prone to adversary's cyber attacks. However, cyber attack detection in such cyber-physical DC power systems has not been systematically investigated yet. To fill the gap, this work successfully synergizes the ideas from two different, yet complementary research communities: power electronics in electrical engineering and formal methods in computer science. Formal verification requires extensive analysis of a given mathematical model with respect to some correctness requirements using various tools and techniques. The challenge of cyber attack detection is investigated to present two solutions using two different techniques from the formal verification community: invariant change detection and signal temporal logic (STL). In the first solution, a framework is presented to detect possible false-data injection attacks (FDIA) 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. The hybrid automaton modeling of cyber-physical DC microgrids is formally presented and reachability analysis is performed for formal verification. In the second solution, STL-based detection of two major types of cyber attacks, FDIA and denial-of-service (DoS) attacks, is presented. STL is a time-dependent logic to evaluate the satisfaction of a dense-time real-valued signal corresponding to a given property. Besides detection, this technique also provides a quantitative measure of the attack impact, called attack impact measure (AIM). As a result, the proposed technique provides a more comprehensive picture of the prevalent cyber-attacks detection. Moreover, it can effectively be employed for complex DC distribution networks without any knowledge of the model. Therefore, this analytical/experimental work employs formal verification techniques to guarantee safe operation of DC power distribution networks in mission-critical and safety-critical applications under hostile cyber attack scenarios.
Keywords
Cyber-physical systems, DC microgrids, DoS attack, False-data injection attack, Formal verification, Hybrid automaton, Hyperproperty, Reachability analysis, Signal temporal logic
Disciplines
Electrical and Computer Engineering | Engineering
License
This work is licensed under a Creative Commons Attribution-NonCommercial-Share Alike 4.0 International License.
Recommended Citation
Beg, Omar Ali, "Formal Verification of DC Distribution Networks" (2017). Electrical Engineering Dissertations. 398.
https://mavmatrix.uta.edu/electricaleng_dissertations/398
Comments
Degree granted by The University of Texas at Arlington