论文标题
FASIM：一个自动分析线性模拟电路模型的框架
FASiM: A Framework for Automatic Formal Analysis of Simulink Models of Linear Analog Circuits
论文作者
论文摘要
Simulink是一个图形环境，广泛适用于建模和基于LapLace转换的基于信号处理体系结构中使用的线性模拟电路的分析。但是，由于MATLAB的数值算法参与了分析过程，因此分析结果不能称为完整和准确。高阶定理证明是一种正式的验证方法，最近提出了为了克服建模和基于拉普拉斯变换的线性模拟电路分析的这些局限性。但是，由于缺乏在行业工作的工程师的形式背景，因此系统的正式建模并不是一项简单的任务。此外，由于高阶逻辑的不确定性，该分析通常需要在手动证明过程中大量的用户指导。为了促进工业工程师根据拉普拉斯变换正式分析线性模拟电路，我们提出了一个框架Fasim，该框架允许使用HOL Light Theorem prover自动对线性模拟电路的Simulink模型进行正式分析。为了进行说明，我们使用FASIM正式分析了一些常用的线性模拟过滤器（例如Sallen-key滤镜）的模型。
Simulink is a graphical environment that is widely adapted for the modeling and the Laplace transform based analysis of linear analog circuits used in signal processing architectures. However, due to the involvement of the numerical algorithms of MATLAB in the analysis process, the analysis results cannot be termed as complete and accurate. Higher-order-logic theorem proving is a formal verification method that has been recently proposed to overcome these limitations for the modeling and the Laplace transform based analysis of linear analog circuits. However, the formal modeling of a system is not a straightforward task due to the lack of formal methods background for engineers working in the industry. Moreover, due to the undecidable nature of higher-order logic, the analysis generally requires a significant amount of user guidance in the manual proof process. In order to facilitate industrial engineers to formally analyze the linear analog circuits based on the Laplace transform, we propose a framework, FASiM, which allows automatically conducting the formal analysis of the Simulink models of linear analog circuits using the HOL Light theorem prover. For illustration, we use FASiM to formally analyze Simulink models of some commonly used linear analog filters, such as Sallen-key filters.
