Formalization of Transform Methods using Higher-order-logic Theorem Proving

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 safety-critical 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 higher-order 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

Untitled

 

HOL Script

 

Publications

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

  2. A. Rashid and O. Hasan, “Formal Analysis of Continuous-time Systems using Fourier Transform”, Journal of Symbolic Computation, Elsevier, Volume 90, pp. 65-88, 2018.

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

Conference Papers
  1. A. Rashid, U. Siddique and O. Hasan, “Formal Verification of Platoon Control Strategies”, International Conference on Software Engineering and Formal Methods (SEFM-2018), Springer, LNCS 10886, Toulouse, France, pp. 223-238.

  2. A. Rashid and O. Hasan, “Formal Analysis of Linear Control Systems using Theorem proving”, International Conference on Formal Engineering Methods (ICFEM-2017), Springer, LNCS 10610, Xian, China, pp. 345-361.

  3. A. Rashid and O. Hasan, “Formalization of Transform Methods using HOL Light”, Conference on Intelligent Computer Mathematics (CICM-2017), Springer, LNAI 10383, Edinburgh, UK, pp. 319-332.

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

  5. 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
  1. A. Rashid and O. Hasan, “Formalization of Fourier Transform using HOL-Light”, Technical Report, NUST, Islamabad, Pakistan, 2017.

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