Obtaining Highly Dependable Communication Protocols

通信协议构成了许多复杂软件系统的组成部分。在许多这样的系统中，协议对系统可靠性的影响远远超过用于实现它们的代码行总数的一小部分。遗憾的是，几乎没有一种系统的方法来设计和评估考虑可靠性的协议，在此之前，我们开发了一种系统的、半自动的通信协议验证方法。我们的方法使用协议的半形式化表示和高效搜索(前向搜索和面向故障的测试生成)来分析整个场景范围内的协议，包括外部事件、故障(例如分组丢失、通信链路故障、通信节点中的状态丢失等)以及网络拓扑。我们的方法的有效性已经通过它在不同范围的协议中的应用来证明。在这个项目中，我们将承担三项主要任务。首先，我们将扩展我们之前开发的框架，为NASA和HDCCSR社区感兴趣的现有协议计算适当的可靠性度量值。其次，我们将开发第一个系统方法来设计满足所需可靠性标准的新协议。最后，我们将使用NASA提供的试验台，结合NASA和其他HDCCSR研究人员提供的专业知识和软件来微调我们的方法，并证明：(I)确实可以使用系统的、半自动的方法为现有通信协议计算可靠性度量的精确值，(Ii)可以以系统的、半自动的方式设计新的协议，以满足所需的可靠性标准，以及(Iii)通信协议可靠性的增强确实可以显著提高NASA和HDCCSR社区感兴趣的许多软硬件系统的可靠性。除了上述技术贡献外，拟议的研究还将对社会产生更广泛的影响。首先，拟议的研究结果将使关键基础设施的可靠性得到改善，例如空中交通管制系统。其次，研究将开发新的方法和实际案例研究，这将为我们提供一个独特的机会，教育大量和多样化的学生群体开发可靠的协议和系统的技术。

Communication protocols form an integral part of many complex software systems. In many such systems, protocols' impact onsystem dependability far exceeds the fraction of the total number of lines of code devoted to their implementation. Unfortunately, there exists virtually no systematic approach for design and evaluation of protocols that considers dependability.Previously, we have developed a systematic, semi-automatic approach for validation of communication protocols. Our approach uses semi-formal representations of protocols and efficient search (forward search as well as fault-oriented test generation) to analyze protocols over the entire range of scenarios, including external events, faults (such as loss of packets, communication link failures, loss of state in communication nodes, and so on), as well as network topologies. The effectiveness of our approach has been demonstrated via its application to a varied range of protocols.In this project, we will undertake three main tasks. First, we will extend our previously developed framework to compute values of appropriate dependability metrics for existing protocols of interest to the NASA and the HDCCSR community. Second, we will develop the first systematic approach to design new protocols that satisfy desired dependability criteria. Finally, we will use the testbed provided by NASA in conjunction with the expertise and software made available by NASA and other HDCCSR researchers to fine-tune our approaches and to demonstrate that: (i) accurate values of dependability metrics can indeed be computed for existing communication protocols using a systematic, semi-automatic approach, (ii) new protocols can be designed in a systematic, semi-automated manner to meet desired dependability criteria, and (iii) enhancements in the dependability of communication protocols can indeed significantly enhance the dependabilities of many software-hardware systems of interest to NASA and the HDCCSR community. In addition to above technical contributions, the proposed research will have broader impact on society. First, results of the proposed research will enable improvements in dependability of critical infrastructure, such as the air-traffic control system. Second, the research will develop new approaches and practical case studies that will provide us with a unique opportunity to educate a large and diverse student body in techniques for development of dependable protocols and systems.