基于定理证明的控制系统属性形式验证
Formal Verification of Control Systems Properties with Theorem Proving
AI总结：
本文提出利用Why3工具对控制系统高阶属性进行演绎形式验证，包括稳定性、反馈增益和鲁棒性等。通过Simulink建模，提出三种主要步骤：指定模型信号属性、自动转换为Why3代码、自动验证属性。
摘要：
本文提出利用定理证明方法对控制系统高阶属性进行演绎形式验证，使用Why3工具。可验证的属性包括稳定性、反馈增益和鲁棒性等。对于在Simulink中建模的系统，我们提出三个主要步骤：使用Simulink块在模型中指定感兴趣的属性，自动将模型转换为Why3，以及自动使用Why3中的定理证明器验证属性。我们提出了一种在模型中指定属性的方法，并开发了一个相关的断言块库（逻辑表达式）。Simulink模型中的块功能通过MATLAB实现的工具自动转换为Why3中的理论和验证目标。已开发出对应的Why3理论库，以促进转换过程。目标通过Why3中的相关定理证明器自动验证。用一个简单的离散系统来举例说明Simulink模型的指定、Simulink到Why3形式逻辑语言的转换过程，以及Lyapunov稳定性验证。
英文摘要：
This paper presents the deductive formal verification of high-level properties of control systems with theorem proving, using the Why3 tool. Properties that can be verified with this approach include stability, feedback gain, and robustness, among others. For the systems, modelled in Simulink, we propose three main steps to achieve the verification: specifying the properties of interest over the signals within the model using Simulink blocks, an automatic translation of the model into Why3, and the automatic verification of the properties with theorem provers in Why3. We present a methodology to specify the properties in the model and a library of relevant assertion blocks (logic expressions), currently in development. The functionality of the blocks in the Simulink models are automatically translated to Why3 as theories and verification goals by our tool implemented in MATLAB. A library of theories in Why3 corresponding to each supported block has been developed to facilitate the process of translation. The goals are automatically verified in Why3 with relevant theorem provers. A simple first-order discrete system is used to exemplify the specification of the Simulink model, the translation process from Simulink to the Why3 formal logic language, and the verification of Lyapunov stability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
