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. Conventionally, systems modeled using topology matrices have been analyzed through paper-and-pencil based proofs or computer-based simulation methods. However, these approaches are unable to provide an accurate analysis due to their inherent limitations, such as human-error proneness and the reliance on unverified algorithms in the core of the associated tools. On the other hand, formal methods, in particular higher-order logic theorem proving, provide computer-based
mathematical reasoning tools for the accurate and sound analysis of network topology matrices.
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. Each 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, in Isabelle/HOL, of several physical systems from the domains of electrical circuits and mechanical kinematics. For instance, based on the formalizations of Kirchhoff’s voltage and current laws, Ohm’s law and Kirchhoff’s index, we analyze generic models of electrical circuit networks, such as Δ−Y and Π−L circuit topologies and a resistive bridge circuit network. We also formally analyze an industrial Epicyclic bevel gear train mechanism by integrating the notion of screw theory to describe the topology and kinematics of a Bendix wrist mechanism and prove the correctness of its kinematic equations.