参数化可重构系统的局部推理
Local Reasoning about Parametric and Reconfigurable Component-based Systems
摘要：
我们引入了一个逻辑框架的规范和基于组件的系统，其中许多组件实例是活跃的，但他们的数量的界限是未知的验证。除了指定和验证参数化系统，我们考虑的方面的动态重构，其中组件可以在运行时迁移的物理地图上，其形状和大小可能会改变。我们描述了这样的参数和可重构的架构，使用资源逻辑，接近的精神分离逻辑，用于推理动态指针结构。这些逻辑支持本地推理的原则，这是编写模块化规范和构建可扩展验证算法的关键，可处理大型工业规模的系统。
英文摘要：
We introduce a logical framework for the specification and verification of component-based systems, in which finitely many component instances are active, but the bound on their number is not known. Besides specifying and verifying parametric systems, we consider the aspect of dynamic reconfiguration, in which components can migrate at runtime on a physical map, whose shape and size may change. We describe such parametric and reconfigurable architectures using resource logics, close in spirit to Separation Logic, used to reason about dynamic pointer structures. These logics support the principle of local reasoning, which is the key for writing modular specifications and building scalable verification algorithms, that deal with large industrial-size systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
