• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Software and systems modeling >Component-based verification using incremental design and invariants
【24h】

Component-based verification using incremental design and invariants

机译：使用增量设计和不变式的基于组件的验证

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are obtained by combining local invariants of their constituent components with interaction invariants that take interactions into account. We study new techniques for computing interaction invariants. Some of these techniques are incremental, i.e., interaction invariants of a composite hierarchically structured component are computed by reusing invariants of its constituents. We formalize incremental construction of components in the BIP language as the process of building progressively complex components by adding interactions (synchronization constraints) to atomic components. We provide sufficient conditions ensuring preservation of invariants when new interactions are added. When these conditions are not satisfied, we propose methods for generating new invariants in an incremental manner by reusing existing invariants from the constituents in the incremental construction. The reuse of existing invariants reduces considerably the overall verification effort. The techniques have been implemented in the D-Finder toolset. Among the experiments conducted, we have been capable of verifying safety properties and deadlock-freedom of sub-systems of the functional level of the DALA autonomous robot. This work goes far beyond the capacity of existing monolithic verification tools.
机译：我们提出基于不变的技术，以有效验证基于组件的系统的安全性和无死锁特性。组件及其交互以BIP语言描述。复合组件的全局不变量是通过将其组成组件的局部不变量与考虑交互作用的交互不变量相结合而获得的。我们研究了计算交互不变性的新技术。这些技术中的一些是增量技术，即，通过重新使用其组成部分的不变性来计算复合分层结构组件的交互不变量。我们将BIP语言中组件的增量构造形式化为通过向原子组件添加交互（同步约束）来构造逐渐复杂的组件的过程。我们提供了充分的条件，以确保在添加新的交互时保留不变量。当不满足这些条件时，我们提出了通过在增量构造中重用来自成分的现有不变式来增量生成新不变式的方法。现有不变量的重用大大减少了整个验证工作。该技术已在D-Finder工具集中实现。在进行的实验中，我们已经能够验证DALA自主机器人功能级别的子系统的安全性和无死锁。这项工作远远超出了现有整体验证工具的能力。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号