• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Proceedings of the IEEE >Formal Verification of Fault-Tolerant Startup Algorithms for Time-Triggered Architectures: A Survey
【24h】

Formal Verification of Fault-Tolerant Startup Algorithms for Time-Triggered Architectures: A Survey

机译：时间触发型体系结构的容错启动算法的形式验证：一项调查

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

摘要

Time-triggered architectures form an important component of many distributed computing platforms for safety-critical real-time applications such as avionics and automotive control systems. TTA, FlexRay, and TTCAN are examples of such time-triggered architectures that have been popular in recent times. These architectures involve a number of algorithms for synchronizing a set of distributed computing nodes for meaningful exchange of data among them. The algorithms include a startup algorithm whose job is to integrate one or more nodes into the group of communicating nodes. The startup algorithm runs on every node when the system is powered up, and again after a failure occurs. Some critical issues need to be considered in the design of the startup algorithms, for example, the algorithms should be robust under reasonable assumptions of failures of nodes and channels. The safety-critical nature of the applications where these algorithms are used demands rigorous verification of these algorithms, and there have been numerous attempts to use formal verification techniques for this purpose. This paper focuses on various formal verification efforts carried out for ensuring the correctness of the startup algorithms. In particular, the verification of different startup algorithms used in three time-triggered architectures, TTA, FlexRay, and TTCAN, is studied, compared, and contrasted. Besides presenting the various verification approaches for these algorithms, the gaps and possible improvements on the verification efforts are also indicated.
机译：时间触发的体系结构构成了许多分布式计算平台的重要组成部分，用于航空电子和汽车控制系统等对安全至关重要的实时应用。 TTA，FlexRay和TTCAN就是这种时间触发体系结构的例子，这种体系结构最近很流行。这些体系结构涉及许多算法，这些算法用于同步一组分布式计算节点，以便在它们之间进行有意义的数据交换。该算法包括启动算法，该启动算法的工作是将一个或多个节点集成到一组通信节点中。当系统加电时，启动算法在每个节点上运行，并且在发生故障后再次运行。在设计启动算法时，需要考虑一些关键问题，例如，在合理假设节点和通道故障的情况下，算法应具有鲁棒性。使用这些算法的应用程序的安全性至关重要，因此需要对这些算法进行严格的验证，并且为此进行了许多尝试使用形式验证技术。本文着重于为确保启动算法正确性而进行的各种形式验证工作。特别是，研究，比较和对比了三种时间触发架构（TTA，FlexRay和TTCAN）中使用的不同启动算法的验证。除了介绍这些算法的各种验证方法外，还指出了验证工作的差距和可能的改进。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号