Related Experiment Video
Updated: Nov 9, 2025
08:33
Author Spotlight: An Optimized Automated Method for Investigating Retinoic Acid Receptors in Neuronal Mitochondria
Published on: July 28, 2023
765
Formal verification of Matrix based MATLAB models using interactive theorem proving
Ayesha Gauhar1, Adnan Rashid1, Osman Hasan1
1School of Electrical Engineering and Computer Science (SEECS), National University of Sciences and Technology (NUST), Islamabad, Pakistan.
Peerj. Computer Science
|April 9, 2021
Summary
This study introduces a library and translator for converting MATLAB models to higher-order logic, enabling formal verification of complex systems. This approach enhances model analysis beyond traditional simulation methods.
Area of Science:
- Computer Science
- Electrical Engineering
- Formal Methods
Background:
- MATLAB is a widely used high-level programming language for modeling and analyzing systems in engineering and science.
- Traditional analysis methods like simulation and debugging offer limited coverage due to inherent incompleteness.
- Formal verification offers enhanced coverage but requires challenging and time-consuming development of formal models, especially for higher-order-logic models.
Purpose of the Study:
- To facilitate the formal verification of MATLAB models by reducing the effort required to develop formal models.
- To present a library of higher-order-logic functions for common MATLAB matrix functions.
- To introduce a translator for automatic conversion of MATLAB models to higher-order logic.
Main Methods:
- Developed a library of higher-order-logic functions mirroring commonly used MATLAB matrix functions.
- Created a translator for automatic conversion of MATLAB models into higher-order logic representations.
- Utilized the HOL Light theorem prover for formal verification of the converted models.
Main Results:
- Successfully created a library of higher-order-logic functions and an automatic translator for MATLAB models.
- Demonstrated the approach by formally analyzing a Finite Impulse Response (FIR) filter model.
- The formal models were successfully verified within the HOL Light theorem prover.
Conclusions:
- The proposed library and translator significantly simplify the process of formally verifying MATLAB models.
- This approach overcomes the limitations of traditional simulation and debugging methods.
- Enables rigorous formal analysis of complex systems modeled in MATLAB, enhancing reliability and correctness.
Related Concept Videos
01:29Mathematical Modeling: Problem Solving
76
Mathematical modeling transforms real-world scenarios into mathematical expressions, allowing for structured problem-solving and analysis. This process involves defining the situation, assigning variables to measurable quantities, selecting an appropriate model, and solving the resulting equation. Such models are invaluable in finance, providing precise methods to evaluate investments, loans, and repayment structures.A widely used example is the calculation of fixed monthly payments on a loan,...
76
01:24Introduction to MATLAB
431
MATLAB stands for Matrix Laboratory. MathWorks developed MATLAB as a multi-paradigm numerical computing environment and proprietary programming language. It has evolved significantly over the years to become a tool utilized by engineers, scientists, and mathematicians for various tasks, including matrix calculations, developing algorithms, data analysis, and visualization. MATLAB's applications span various industries and disciplines. It's used in image and signal processing,...
431
01:12Theorems of Pappus and Guldinus: Problem Solving
892
Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...
892
01:20Relation between Mathematical Equations and Block Diagrams
2.5K
In a spring-mass-damper system, the second-order differential equation describes the dynamic behavior of the system. When transformed into the Laplace domain under zero initial conditions, this equation can be effectively analyzed and manipulated. The transformation into the Laplace domain converts differential equations into algebraic equations, simplifying the process of isolating the output.
2.5K
01:30Fundamental Theorem of Algebra
46
The Fundamental Theorem of Algebra is central to the study of polynomial equations, asserting that every non-constant polynomial with complex coefficients has at least one complex zero. This means that a polynomial of degree n ≥ 1, written as: with an ≠ 0, has at least one solution in the complex number system. Since the set of real numbers is a subset of complex numbers, this theorem applies equally to polynomials with real coefficients.Building on this result, the Complete...
46
01:15Thevinin's Theorem
1.1K
Thévenin's theorem plays a pivotal role in electrical circuit analysis, offering a solution to the challenges posed by variable loads within a circuit. In practical applications, it is common to encounter circuits where certain elements remain fixed while others fluctuate, often referred to as the "load." A typical household electrical outlet serves as a prime example of a variable load, as it can be connected to a variety of appliances, each with its own unique electrical characteristics.
1.1K