论文标题
线性动力学系统的基于模拟的假设合同的串联组成
Series composition of simulation-based assume-guarantee contracts for linear dynamical systems
论文作者
论文摘要
我们介绍了具有输入和输出的连续时间线性动力学系统的假定保证合同。这些合同用于表达有关系统动态行为的规格。与现有方法相反，我们使用模拟比较两个系统的动态行为。这具有通过有效的数值算法来支持验证的优势，以及与基于（BI）基于仿真的技术的丰富文献有关验证和控制的技术，例如基于（离散的）抽象的技术。使用模拟，我们定义合同实施和合同精致概念。我们还为合同定义了串联组成的概念，这使我们能够根据其组件上的合同来推论系统的系列互连。加在一起，改进和组成的概念允许合同用于互连系统的模块化设计和分析。
We present assume-guarantee contracts for continuous-time linear dynamical systems with inputs and outputs. These contracts are used to express specifications on the dynamic behaviour of a system. Contrary to existing approaches, we use simulation to compare the dynamic behaviour of two systems. This has the advantage of being supported by efficient numerical algorithms for verification as well as being related to the rich literature on (bi)simulation based techniques for verification and control, such as those based on (discrete) abstractions. Using simulation, we define contract implementation and a notion of contract refinement. We also define a notion of series composition for contracts, which allows us to reason about the series interconnection of systems on the basis of the contracts on its components. Together, the notions of refinement and composition allow contracts to be used for modular design and analysis of interconnected systems.
