Abstract:
In the last two decades fractional order systems, which involve integration and dif ferentiation of non-integer order, have become very popular in the fields of control
systems, robotics, signal processing and circuit theory. Traditionally, the analy sis of fractional order systems has been performed using paper-and-pencil based
proofs or computer algebra systems. These analysis techniques compromise the ac curacy of their results and thus are not recommended to be used for safety-critical
fractional order systems. In the past couple of decades, formal methods have been
successfully used for the precise analysis of a variety of hardware and software
systems. The rigorous exercise of developing a mathematical model for the given
system and analyzing this model using mathematical reasoning usually increases
the chances for catching subtle but critical design errors that are often ignored
by traditional techniques like numerical methods. Given the sophistication of the
present age fractional order systems and their extensive usage in safety-critical
applications, there is a dire need of using formal methods in this domain. This
thesis proposes to use higher-order logic theorem proving to analyze fractional or der systems; the main reason being the highly expressive nature of higher-order
logic, which can be leveraged upon to essentially model any system that can be
expressed in a closed mathematical form.
In particular, this thesis provides higher-order logic formalization of the Gamma
function along with the verification of its classical properties using the HOL theo rem prover. We build upon the Gamma function for the formalization of Fractional
Calculus based on the Riemann-Liouville approach and verify its key properties
such as identity, relation to integer order calculus and linearity. This formalization
framework can be used to formalize and verify the properties of fractional order
systems within the sound core of HOL theorem prover. In order to demonstrate
the usefulness of current work, we utilize it to formalize fractional electrical com ponent Resistoductance, fractional integrator and differentiator circuits and then
verify their output response to benchmark input signals.
