Adnan Rashid and Osman Hasan
Abstract
Algebraic techniques based on transform methods are widely used for solving differential equations and evaluating transfer function, and frequency response of signals while analyzing physical aspects of many safetycritical systems. In this project, we facilitate the formal analysis of these systems by providing the formalization of transform methods (the Laplace and the Fourier transforms) using the multivariable calculus theories of HOL Light. In particular, we use integral, differential, vectors, Lp spaces, transcendental and topological theories of multivariable calculus to formally define the Laplace and the Fourier transforms in higherorder logic and reason about the correctness of their properties, such as integrability, linearity, frequency shifting, modulation, time shifting, time scaling, time reversal, differentiation and integration in time domain, uniqueness, relationship of the Laplace and the Fourier transforms, and relationship of the Fourier transform with Fourier Cosine and Sine transforms. In order to demonstrate the practical effectiveness of our proposed formalization, we use it to formally verify some commonly used electrical circuits, an automobile suspension system, an audio equalizer, a MEMs accelerometer, controllers and compensators, 4π soft error crosstalk model, pitch control of an unmanned free swimming submersible vehicle and control strategies for platoon of automated vehicles.
Framework
HOL Script
Publications
Journal Papers

A. Rashid and O. Hasan, “Formalization of Lerch’s Theorem using HOL Light”, Journal of Applied Logic, (Accepted in June 2018).

A. Rashid and O. Hasan, “Formal Analysis of Continuoustime Systems using Fourier Transform”, Journal of Symbolic Computation, Elsevier, Volume 90, pp. 6588, 2018.

S.H. Taqdees and O. Hasan, “Formally Verifying Transfer Functions of Linear Analog Circuits”, IEEE Design & Test, Volume 34, Issue 5, pp. 3037, 2017.
Conference Papers

A. Rashid, U. Siddique and O. Hasan, “Formal Verification of Platoon Control Strategies”, International Conference on Software Engineering and Formal Methods (SEFM2018), Springer, LNCS 10886, Toulouse, France, pp. 223238.

A. Rashid and O. Hasan, “Formal Analysis of Linear Control Systems using Theorem proving”, International Conference on Formal Engineering Methods (ICFEM2017), Springer, LNCS 10610, Xian, China, pp. 345361.

A. Rashid and O. Hasan, “Formalization of Transform Methods using HOL Light”, Conference on Intelligent Computer Mathematics (CICM2017), Springer, LNAI 10383, Edinburgh, UK, pp. 319332.

A. Rashid and O. Hasan, “On the Formalization of Fourier Transform in Higherorder Logic”, Interactive Theorem Proving (ITP 2016), Springer, LNCS 9807, Nancy, France, pp. 483490. (Rank A, CORE)

S.H. Taqdees and O. Hasan, “Formalization of Laplace Transform Using the Multivariate Calculus Theory of HOL Light”, Logic for Programing Artificial Intelligence and Reasoning (LPAR 2013), Springer LNCS 8312, Stellenbosch, South Africa, pp. 744–758. (Rank A, CORE)
Technical Reports

A. Rashid and O. Hasan, “Formalization of Fourier Transform using HOLLight”, Technical Report, NUST, Islamabad, Pakistan, 2017.

A. Rashid and O. Hasan, “Formal Analysis of Linear Control Systems using Theorem Proving”, Technical Report, NUST, Islamabad, Pakistan, 2017.