FASiM：一种用于线性模拟电路 Simulink 模型自动形式化分析的框架
计算机科学中的逻辑
2020-01-22 v1
摘要
Simulink 是一种被广泛用于信号处架构中线性模拟电路建模及基于拉普拉斯变换分析的图形化环境。然而，由于分析过程中涉及 MATLAB 的数值算法，分析结果不能被称为完整且准确的。高阶逻辑定理证明是近来提出的用于克服线性模拟电路建模及基于拉普拉斯变换分析这些局限性的形式化验证方法。然而，由于工业界工程师缺乏形式化方法背景，系统的形式化建模并非一项直截了当的任务。此外，由于高阶逻辑不可判定的性质，分析通常在手动证明过程中需要大量的用户引导。为了便于工业界工程师基于拉普拉斯变换对线性模拟电路进行形式化分析，我们提出了一个框架 FASiM，它允许使用 HOL Light 定理证明器自动对线性模拟电路的 Simulink 模型进行形式化分析。为说明起见，我们使用 FASiM 对一些常用线性模拟滤波器（如 Sallen-key 滤波器）的 Simulink 模型进行了形式化分析。
引用
@article{arxiv.2001.06702,
title = {FASiM: A Framework for Automatic Formal Analysis of Simulink Models of Linear Analog Circuits},
author = {Adnan Rashid and Ayesha Gauhar and Osman Hasan},
journal= {arXiv preprint arXiv:2001.06702},
year = {2020}
}