Formalization Of Laplace Transform In Coq And Its Application In Flight Control System Verification

Formalized mathematics is a research direction for mechanical verification of mathematical theorems by means of theorem prover.Formalized engineering mathematics is the application of formalized mathematics in the field of engineering mathematics.A key mathematical tool in the design of control systems is the Laplace transform,which is widely used to solve linear differential equations and analyze safety critical systems.It is also a basic tool for many control algorithms design and software design,including flight control systems.Theorem proving is a technique to help people to prove mathematical theorems under the assistance of computers.It overcomes the shortcomings of paper-and-pencil method traditionally which is human-error prone.It has been widely used in mathematical proving,integrated circuit and software verification.However,Formal verification in flight control is rare.A promising example is the adoption of SCADE system for modeling,developing and verifying the flight control software.Although model based methodology increases software productivity and reduces software bugs,they do not address the reliability of the mathematical derivation of models,which often involves manipulation of complicated mathematical formulas.To address this problem,we take the approach of formalization of engineering mathematics.More specifically,we are attempting to work in the direction of developing a databases of formal engineering mathematics in the proof assistant Coq.This is certainly a long term and ambitious project,and this paper is one of the initial steps towards this goal.This particular problem studied in this paper is to formalize the Laplace transform in Coq and verify the practical problems in the flight control systems.In this paper,the formal definition of Laplace transform are realized by the theory of limit,continuity,differentiation,integration,complex numbers in the high-order logic theorem prover Coq.A group of basic properties of Laplace transform are verified,including existence,linear property,frequency shifting,first order differentiation,second-order differentiation and integration property,etc.In order to verify more complex control systems,we extends the formalization of Laplace transform from one dimensional to two dimensional,and the main properties of two dimensional Laplace transform are also proved.This basic work has been able to effectively support the formal verification of most control systems in practical applications.The implement of two dimensional Laplace transform relies on formal theories of matrix.We use a tuple-based representation method to formally define small-scale matrices(2-4 dimensions)and formalize the operations of matrices,operations on vectors,and operations between matrices and vectors.On this basis,the correctness and the natures of these matrix operations are also formally proved in Coq.Finally,we formally verified the derivation process of some transfer functions in flight control systems and robot control systems.