Formal Verification of Coupled Transmission Lines using Theorem Proving
摘要
Coupled transmission lines are essential components of modern electronic systems, which facilitate a reliable and an efficient transmission of high-frequency signals from source to destination and are widely used in various industries, including telecommunications, aerospace, and automotive. Moreover, their dynamics are generally represented by a set of differential equations involving voltages and currents, known as the telegrapher’s equations. This paper proposes to use Higher-Order Logic (HOL) theorem proving for formal modeling and verification of coupled transmission lines. In particular, we formalize the equations capturing the line voltages and currents, and their relationship in a system of coupled transmission lines. We then formally verify the equivalence between these equations and their matrix representations. Finally, we conduct a formal proof of the correctness of the general solutions of these generalized telegrapher’s equations using the HOL Light theorem prover.