全波整流器的形式化验证：一个案例研究
计算机科学中的逻辑
2016-11-17 v1
摘要
我们提出了一个针对模拟与混合信号设计的全波整流器形式化验证的案例研究。我们使用了来自CMU的Checkmate工具[1]，这是一个用于混合系统的公共领域形式化验证工具。由于Checkmate施加的限制，有必要对Checkmate的实现进行修改，以实现复杂和非线性系统。全波整流器通过使用Checkmate自定义模块和来自MathWorks的MATLAB中的Simulink模块实现。在对Checkmate实现进行必要的修改后，我们能够有效地验证全波整流器的安全属性。
引用
@article{arxiv.0909.5393,
title = {Formal Verification of Full-Wave Rectifier: A Case Study},
author = {Kusum Lata and H S Jamadagni},
journal= {arXiv preprint arXiv:0909.5393},
year = {2016}
}
备注
The IEEE 8th International Conference on ASIC (IEEE ASICON 2009), October 20-23 2009, Changsha, China