Formalization of Partial Differential Equations using HOL Theorem Proving
Elif Deniz, Adnan Rashid and Sofiene Tahar
Contact: e_deniz@encs.concordia.ca
Partial Differential Equations (PDEs) are used in modeling important engineering and physical science problems, such as the motion of fluids, the flow of current in electric circuits or the dissipation of heat in solid objects. Among the most well-known examples of PDEs are the Maxwell and the telegrapher's equations in electromagnetic theory, the Laplace equation for fluid dynamics, the wave equation for the description of waves, and the heat equation for describing the diffusion of heat. The main objective of this research project is to develop a framework, based on higher-order logic theorem proving, for the mathematical modeling, analysis and verification of physical systems described by PDEs. In particular, we formalize the heat, Laplace, telegrapher's and wave equations and verify their solutions using the HOL-Light theorem prover. We then use our framework to analyze several physical systems such as thermal protection, potential flows and electrical transmission lines.
[2] Deniz, E., Rashid, A., Tahar, S. Formal Verification of Coupled Transmission Lines. International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), Lecture Notes in Computer Science (LNCS), Springer, Djerba, Tunisia, TO APPEAR (2024).
[3] Deniz, E., Rashid, A., Hasan, O., Tahar, S. Formal Verification of ABCD Parameters Based Models for Transmission Lines. In: S.M. Watt and T. Ida (Eds.), Symbolic Computation in Software Science, Lecture Notes in Computer Science 14991, Springer Verlag, 2024, pp. 20-37. [Proc. Symposium on Symbolic Computation in Software (SCSS'2024), Tokyo, Japan, August 2024].
[4] Deniz, E., Rashid, A., Hasan, O., Tahar, S. On the Formalization of the Heat Conduction Problem in HOL. International Conference on Intelligent Computer Mathematics (CICM’22), Lecture Notes in Artificial Intelligence (LNAI), Springer, Vol. 13467, pp: 21-37, Tbilisi, Georgia (2022).
Publications
Journal Papers
[1] Deniz, E., Rashid, A., Hasan, O., Tahar, S. Formalization of the Telegrapher’s Equations using Higher-Order-Logic Theorem Proving. Journal of Applied Logics, 11(2) (2024).Conference Papers
[1] E. Deniz and S. Tahar: Formalizing Potential Flows using the HOL Light Theorem Prover; In: K. Ogata, D. Mery, M. Sun, and S. Liu (Eds.), Formal Methods and Software Engineering, Lecture Notes in Computer Science 15394, Springer Verlag, 2024, pp. 297-313. [Proc. International Conference on Formal Engineering Methods (ICFEM’24), Hiroshima, Japan, December 2024][2] Deniz, E., Rashid, A., Tahar, S. Formal Verification of Coupled Transmission Lines. International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), Lecture Notes in Computer Science (LNCS), Springer, Djerba, Tunisia, TO APPEAR (2024).
[3] Deniz, E., Rashid, A., Hasan, O., Tahar, S. Formal Verification of ABCD Parameters Based Models for Transmission Lines. In: S.M. Watt and T. Ida (Eds.), Symbolic Computation in Software Science, Lecture Notes in Computer Science 14991, Springer Verlag, 2024, pp. 20-37. [Proc. Symposium on Symbolic Computation in Software (SCSS'2024), Tokyo, Japan, August 2024].
[4] Deniz, E., Rashid, A., Hasan, O., Tahar, S. On the Formalization of the Heat Conduction Problem in HOL. International Conference on Intelligent Computer Mathematics (CICM’22), Lecture Notes in Artificial Intelligence (LNAI), Springer, Vol. 13467, pp: 21-37, Tbilisi, Georgia (2022).
Source Code
Applications
Heat Transfer
Heat conduction or diffusion is the flow of energy in a system/body from the region of high temperature to the region of low temperature by direct collision of molecules. We opted HOL theorem proving to formally analyze the heat conduction problem in rectangular coordinates. In particular, we modeled the heat transfer as a one-dimensional heat equation for a rectangular slab. We also used the separation of variables method to verify the solution of the heat equation, allowing us to model the heat transfer in the slab under various initial and boundary conditions.
Transmission Lines
Transmission lines are used to carry electrical energy from a generating source to various distribution units by transmitting voltage and current waves from one end to the other. The behavior of transmission lines is elucidated through the utilization of the telegrapher’s equations that are based on Partial Differential Equations (PDEs) and rigorously capture the complex electromagnetics and propagation dynamics occurring within these transmission systems. We formally modeled the telegrapher's equations and verified the correctness of their analytical solutions. We also formally analyzed several practical applications such as terminated, coupled and cascaded transmission lines.
Potential Flows
Potential flow theory is a key concept in the discipline of fluid dynamics. For instance, in aerodynamics, this theory has played a pivotal role in developing analytical models to understand airflow around airfoils, wings, and related aerodynamic surfaces, which in turn facilitate the prediction of crucial aerodynamic forces such as lifts. We conducted the formal specification and verification of standard potential flows solutions which satisfy the Laplace equation. We also formally analyzed several practical applications, including the Rankine oval, potential flow past a circular cylinder and potential flow past a rotating circular cylinder.
Wireless Power Transfer
Wireless Power Transfer (WPT) system enables the transmission of electrical energy from source to destination without establishing a physical connection. A WPT system uses the phenomenon of electromagnetic fields based on the induction coils to send energy from the transmitter to the receiver. We formally verified the T-shaped circuit model for Wireless Power Transfer (WPT) that is widely used in electric vehicles and embedded devices.
