Formalization of Transform Methods using Higher-order-logic Theorem Proving
PhD Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan
Theorem Proving · HOL Light
A foundational formalization of Laplace and Fourier transform methods in HOL Light — the mathematical core behind formal frequency-domain and transfer-function analysis across this research program.
Abstract
Algebraic techniques based on transform methods are widely used for solving differential equations and evaluating transfer functions and frequency response while analyzing physical aspects of safety-critical systems. We present a formalization of transform methods — Laplace and Fourier transforms — using the multivariable calculus theories of HOL Light: integral, differential, transcendental, and topological theories are used to formally define these transforms and verify properties such as existence, linearity, frequency shifting, modulation, time shifting, time scaling, differentiation and integration in the time domain, and their mutual relationships (including with the Fourier Cosine and Fourier Sine transforms).
We demonstrate practical effectiveness by formally verifying commonly used electrical circuits, an automobile suspension system, an audio equalizer, a MEMS accelerometer, controllers and compensators, a 4-π soft-error crosstalk model, and the pitch control of an unmanned free-swimming submersible vehicle.
Framework
Related Publications