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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formal Verification of Coupled Transmission Lines using Theorem Proving

  • Elif Deniz,
  • Adnan Rashid,
  • Sofiène Tahar

摘要

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.