PhD Oral Exam - Kubra Aksoy, Electrical and Computer Engineering

When studying for a doctoral degree (PhD), candidates submit a thesis that provides a critical review of the current state of knowledge of the thesis subject as well as the student’s own contributions to the subject. The distinguishing criterion of doctoral graduate research is a significant and original contribution to knowledge.

Once accepted, the candidate presents the thesis orally. This oral exam is open to the public.

Abstract

Network topology matrices play a central role in the mathematical modeling and analysis of many physical and engineering systems, including electrical networks, power grids, mechanical and robotic systems. They provide compact algebraic representations of networks, and are widely used in modeling system behaviors and deriving governing equations. In this thesis, we propose to use the Isabelle/HOL interactive theorem prover to build a comprehensive framework for the formalization of network topology matrices describing mathematical models of physical systems. In particular, we have developed formal libraries for reasoning about network systems and widely used network topology matrices, namely adjacency, degree, loop, incidence and Laplacian matrices. matrix library includes the formal definitions of these matrices and the formal verification of their fundamental properties, such as indexing, symmetry, singularity, and degree. We also formally verify the relationship between these matrices to ensure the soundness and completeness of their formalizations in Isabelle/HOL. Furthermore, we formalize two well-known matrix algebraic methods, namely, Kron reduction and pseudoinverse. To illustrate the practical utility and effectiveness of our proposed framework, we perform the formal analysis of several physical systems from the domains of electrical circuits and mechanical kinematics. For instance, we formally analyze generic models of electrical circuit networks, such as ∆-Y and II-L circuit topologies and a resistive bridge circuit network. We also performed the formal analysis of an industrial Epicyclic bevel gear train mechanism by describing the topology and kinematics of a Bendix wrist mechanism and proving the correctness of its kinematic equations.