基于断言检查和定理证明的Simulink控制系统验证：案例研究
系统与控制
2021-04-13 v2 软件工程
摘要
本文介绍了在Simulink中实现的控制系统的验证。目标是确保控制性能的高层需求（如稳定性）由Simulink框图满足。提出了一个两阶段过程。首先，将高层需求分解为具体的参数化子需求，并作为断言在Simulink中实现。其次，进行验证。一方面，子需求通过仿真中的断言检查进行验证。另一方面，根据其范围，部分子需求通过仿真中的断言检查验证，其他则通过对框图的理想数学模型进行自动定理证明来验证。我们比较了仅执行断言检查与使用定理证明，以突出后者的优势。定理证明通过符号化计算数学证明来进行验证，覆盖变量的整个状态空间。还提出了一种从Simulink到定理证明工具Why3语言的自动转换工具。本文通过验证一个简单的离散线性系统的稳定性来演示我们的方法。
引用
@article{arxiv.1505.05699,
title = {Verification of Control Systems Implemented in Simulink with Assertion Checks and Theorem Proving: A Case Study},
author = {Dejanira Araiza-Illan and Kerstin Eder and Arthur Richards},
journal= {arXiv preprint arXiv:1505.05699},
year = {2021}
}
备注
Accepted, waiting for publication. European Control Conference, July 2015, Linz, Austria