Search or add a thesis

Advanced Search (Beta)
Home > Formalization of Transform Methods Using Higher-Order-Logic Theorem Proving

Formalization of Transform Methods Using Higher-Order-Logic Theorem Proving

Thesis Info

Access Option

External Link

Author

Rashid, Adnan

Program

PhD

Institute

National University of Sciences & Technology

City

Islamabad

Province

Islamabad

Country

Pakistan

Thesis Completing Year

2019

Thesis Completion Status

Completed

Subject

Computer Science

Language

English

Link

http://prr.hec.gov.pk/jspui/bitstream/123456789/11517/1/Adnan%20Rashid%20Information%20Technology%202019.pdf

Added

2021-02-17 19:49:13

Modified

2024-03-24 20:25:49

ARI ID

1676727762169

Similar


Transform methods, such as the Laplace and the Fourier transforms, are widely used for analyzing the differential equations modeling the continuous dynamics of the engineering and physical systems. Traditionally, the transform methods based analysis is performed using paper-and-pencil proof and computer-based simulation techniques, such as sym bolic and numerical methods. However, due to their inherent limitations, such as the human-error proneness of paper-and-pencil proof methods and the presence of unverified symbolic algorithms, discretization and numerical errors in the simulations methods, these techniques cannot provide accurate results. The incomplete and inaccurate analysis poses a serious threat to the safety-critical domain, such as medicine and transportation, of engineering systems. To overcome these limitations, we propose to use higher-order-logic theorem proving to reason about the continuous dynamics of the engineering and physical systems using transform methods. The main advantages of this approach are the high expressiveness of the higher-order logic and the soundness of theorem provers, which provide absolute accu racy of the analysis. In particular, this thesis presents a higher-order-logic formalization of the Laplace and the Fourier transforms, which includes their formal definitions and the formal verification of their classical properties. The considered properties include integra bility, linearity, time shifting, frequency shifting, modulation, time scaling, time reversal, integration in time domain, differentiation in time domain, the Laplace and the Fourier transforms of a n-order differential equation and uniqueness. The formal reasoning about these properties involves multivariable calculus theories, i.e., the differential, integration, transcendental, topological, complex numbers, Lp spaces and vectors theories. Based on the availability of these theories in the HOL Light theorem prover, we chose it for our work. This thesis also provides the formal verification of a relationship between various transfor methods, i.e., the relationship between the Laplace and the Fourier transforms, and the relationship between the Fourier transform and the Fourier Cosine and Sine transforms. The proposed formalization plays a vital role in formally verifying the solutions of differential equations in both the time and the frequency domain and thus facilitates formal dynamical analysis of these systems. To illustrate the practical utilization and effectiveness, we use our proposed formalization for formally analyzing a 4-π soft error crosstalk model for Integrated Circuits (ICs), an audio equalizer, an Unmanned Free swimming Submersible (UFSS) vehicle and a platoon of automated vehicles using HOL Light.
Loading...

Similar Thesis

Showing 1 to 20 of 100 entries
TitleAuthorSupervisorDegreeInstitute
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National College of Business Administration and Economics, Lahore, Pakistan
Riphah International University, Islamabad, Pakistan
Mehran University of Engineering and Technology, Jamshoro, Pakistan
Mphil
Riphah International University, Islamabad, Pakistan
BS
COMSATS University Islamabad, Islamabad, Pakistan
Phd
COMSATS University Islamabad, Islamabad, Pakistan
PhD
COMSATS University Islamabad, Islamabad, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
PhD
National University of Sciences & Technology, Islamabad, Pakistan
Mphil
Riphah International University, Faisalabad, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
Mphil
Quaid-i-Azam University, Islamabad, Pakistan
Mphil
Quaid-i-Azam University, Islamabad, Pakistan
PhD
National University of Computer and Emerging Sciences, Islamabad, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
MSc
Quaid-i-Azam University, Islamabad, Pakistan
Mehran University of Engineering and Technology, Jamshoro, Pakistan
University of Engineering and Technology, Lahore, Pakistan
TitleAuthorSupervisorDegreeInstitute
Showing 1 to 20 of 100 entries

Similar News

Loading...

Similar Articles

Loading...

Similar Article Headings

Loading...