论文标题
动态系统的假设/担保合同：理论和计算工具
Assume/Guarantee Contracts for Dynamical Systems: Theory and Computational Tools
论文作者
论文摘要
现代工程系统包括许多不同类型和功能的组件。验证这些系统满足给定规格可能是一项艰巨的任务，因为大多数正式验证方法仅限于中等大小的系统。最近，已提出合同理论作为定义规格的模块化框架。在本文中，我们提出了依赖于假设/担保合同的离散时间动态控制系统的合同理论，该系统规定了系统输入的假设并保证输出。然后，我们专注于由线性约束定义的合同，并开发有效的计算工具，以基于线性编程来验证满意度和改进。我们在模拟示例中示例这些工具，证明了两辆车自动驾驶设置的一定安全规范。
Modern engineering systems include many components of different types and functions. Verifying that these systems satisfy given specifications can be an arduous task, as most formal verification methods are limited to systems of moderate size. Recently, contract theory has been proposed as a modular framework for defining specifications. In this paper, we present a contract theory for discrete-time dynamical control systems relying on assume/guarantee contracts, which prescribe assumptions on the input of the system and guarantees on the output. We then focus on contracts defined by linear constraints, and develop efficient computational tools for verification of satisfaction and refinement based on linear programming. We exemplify these tools in a simulation example, proving a certain safety specification for a two-vehicle autonomous driving setting.
