Most of the engineering and physical systems are generally characterized by differential and difference equations based on their continuous-time and discrete-time dynamics, respectively. Moreover, these dynamical models are analyzed using transform methods to prove various properties of these systems, such as, transfer function, frequency response and stability, and to find out solutions of the differential/difference equations. The conventional techniques for performing the transform methods based analysis have been unable to provide an accurate analysis of these systems. Therefore, higher-order-logic theorem proving, a formal method, has been used for accurately analyzing systems based on transform methods. In this paper, we survey developments for transform methods based analysis in various higher-order-logic theorem provers and overview the corresponding real world case studies from the avionics, medicine and transportation domains that have been analyzed based on these developments.
翻译:大多数工程和物理系统一般都具有基于连续时间和离散时间动态的不同和差异方程式的特点,此外,对这些动态模型进行分析时采用变换方法,以证明这些系统的各种特性,如转移功能、频率反应和稳定性,并找出差异/差异方程式的解决办法。基于变换方法分析的常规技术无法对这些系统进行准确分析。因此,根据变换方法准确分析系统时使用了较高顺序的逻辑,这是一种正式方法。在本文件中,我们调查了各种更高顺序理论验证仪中基于变换分析方法的发展动态,并概述了根据这些发展分析的航空、医学和运输领域的相应真实世界案例研究。