Formalization of Continuous Fourier Transform in Verifying Applications for Dependable Cyber-Physical Systems

Continuous Fourier transform (CFT) is widely used and is often directly applied in cyber-physical systems (CPS) without checking its preconditions. This inevitably leads to unexpected defects and even errors. Thus, verification is necessary for the CFT-based engineering design to ensure a dependable cyber physical system. HOL4 (Higher Order Logic 4) is a formal theorem prover that prevails in software and hardware verification. However, there is no CFT theorem library in current HOL4. In this paper, the definition and some frequently used properties of CFT are formalized and verified in HOL4. Based on this, we formally model a basic theorem library of CFT. As a case study, the CFT library is employed to verify the frequency response of an RLC circuit, which is a critical application for dependable CPS. The formalization of the CFT and its properties and the construction of the formal CFT theorem library can effectively extend the function of the HOL4 system. The obtained formal results can be applied in various CFT-based cyber-physical systems.