• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Latin-American Symposium on Dependable Computing(LADC 2005); 20051025-28; Salvador(BR) >Verifying Fault-Tolerant Distributed Systems Using Object-Based Graph Grammars
【24h】

Verifying Fault-Tolerant Distributed Systems Using Object-Based Graph Grammars

机译：使用基于对象的图语法验证容错分布式系统

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

摘要

Assuring the correctness of fault-tolerant distributed systems can be an overwhelming task. Besides dealing with complex problems of distributed systems, it is also necessary to design the system in such a way that a well-defined failure behaviour, or the masking of failure components, is presented by the system when components fail. To help reasoning about such systems, the use of formal methods becomes desirable. In previous work we introduced a graphical formal specification language, called Object-Based Graph Grammars (OBGG), for modelling asynchronous distributed systems. We also defined a method for automatically inserting classical fault behaviours into OBGG models. The obtained models could be analysed using simulation. In this paper a new method for automatically inserting fault behaviours into OBGG models, which is suitable for using verification as the analysis method, is proposed. Moreover, we show how to formally verify OBGG models in the presence of such faults. A two phase commit protocol is used to illustrate the contributions.
机译：确保容错分布式系统的正确性可能是一项艰巨的任务。除了处理分布式系统的复杂问题外，还必须以这样一种方式设计系统，即当组件发生故障时，系统会提供明确定义的故障行为或故障组件的掩盖。为了帮助推理此类系统，需要使用形式化方法。在先前的工作中，我们引入了一种图形化的正式规范语言，称为基于对象的图形语法（OBGG），用于对异步分布式系统进行建模。我们还定义了一种将经典故障行为自动插入到OBGG模型中的方法。获得的模型可以使用仿真进行分析。提出了一种将故障行为自动插入到OBGG模型中的新方法，该方法适合于使用验证作为分析方法。此外，我们展示了如何在存在此类故障的情况下正式验证OBGG模型。使用两阶段提交协议来说明贡献。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号