• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >A modular approach to formal specification and verification of dependable distributed protocols.
【24h】

A modular approach to formal specification and verification of dependable distributed protocols.

机译：正式规范和验证可靠的分布式协议的模块化方法。

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

摘要

Dependable distributed system typically utilize a hierarchy of protocols to provide for reliable and timely services. Such protocols have both dependability and real-time attributes, and the analysis of these protocols is a problem of growing complexity. The development of precise and accurate formal specifications of these protocols and their subsequent formal verification to gain assurance have been a great challenge. Exploiting the inherent modularity in the design of most dependable protocols, in this thesis, we present our modular approach to specification composition and verification of dependable distributed protocol. In particular, we consider redundancy management protocols that are needed to manage redundant resources used in the system for dependability purposes. Utilizing building-block protocols inherently used in redundancy management protocols, we perform compositional specification and verification of a checkpointing and recovery protocol based on them. The key idea is that if a library of these basic components, like the primitives and sub-protocols are being formulated, then these elements aid in systematic and hierarchical development of dependable distributed protocols. The main contribution of this thesis to illustrate the fact that by defining a priori validated building-blocks for dependable distributed protocols, larger and more complex protocols can be easily specified and verified. For a mechanical support in formal verification process, we use formal tools such as Specware and PVS.
机译：可靠的分布式系统通常利用协议的层次结构来提供可靠和及时的服务。这样的协议具有可靠性和实时性，并且对这些协议的分析是日益复杂的问题。这些协议的精确和正式形式规范的发展以及随后的形式验证以获取保证一直是一个巨大的挑战。在开发最可靠协议的固有模块性的基础上，本文提出了一种用于规范组成和可靠分布式协议验证的模块化方法。特别是，我们考虑了出于可靠性目的管理系统中使用的冗余资源所需的冗余管理协议。利用冗余管理协议中固有的构建块协议，我们执行组成规范以及基于它们的检查点和恢复协议的验证。关键思想是，如果正在制定包括这些基本组件（如原语和子协议）的库，那么这些元素将有助于可靠的分布式协议的系统和分层开发。本论文的主要贡献是说明了以下事实：通过为可靠的分布式协议定义先验验证的构建基块，可以轻松地指定和验证更大，更复杂的协议。对于形式验证过程中的机械支持，我们使用形式工具，例如Specware和PVS。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号