Formal Analysis of Fractional Order Systems in Higher-order Logic

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.