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.
