FORMAL ANALYSIS OF HOMOGENEOUS LINEAR DIFFERENTIAL EQUATIONS USING THEOREM PROVING

Abstract

Traditionally, differential equations are solved using paper-and-pencil proof methods, com puter based numerical methods or computer algebra systems. All these methods are error prone and thus the analysis cannot be termed as accurate, which poses a serious threat to the accuracy of the safety-critical systems that involve differential equations. To guarantee the correctness of analysis, we propose to use higher-order-logic theorem proving to reason about the correctness of solutions of differential equations. This thesis presents a formal ization framework to express homogeneous linear differential equation of arbitrary order and formally verify their solutions within the sound core of a higher-order-logic theorem prover HOL4. In order to illustrate the usefulness of the proposed formalization, we utilize it to formally verify the solutions of a couple of safety-critical biomedical systems, namely a heart pacemaker and a fluid-filled catheter, which are one of the most safety-critical systems as their bugs could eventually result in the loss of human lives. We also show the utilization of our work by formally verifying Analog and Mixed Signals (AMS) designs which are widely being used in many integrated circuits. Due to their continuous nature, their analysis has primarily been done with informal techniques, like simulation, or formal methods with abstracted discrete models. This fact makes AMS designs error prone, which may lead to disastrous consequences given the safety and financial critical nature of their applications. Leveraging upon the high expressiveness of higher-order logic, we propose to use higher-order-logic theorem proving to analyze continuous models of AMS designs. To take an example of our foundational AMS design analysis formalization, we present the formal analysis of a classical RLC circuit using the HOL4 theorem prover.