Omar Ali Beg

ORCID Identifier(s)

0000-0002-5353-7616

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

Comments

Degree granted by The University of Texas at Arlington

Download

Share

COinS