Obtaining Highly Dependable Communication Protocols

通信协议是许多复杂软件系统的组成部分。在许多这样的系统中，协议对系统可靠性的影响远远超过了用于实现它们的代码行总数的一小部分。不幸的是，几乎没有系统的方法来设计和评估的协议，考虑可靠性。以前，我们已经开发了一个系统的，半自动的方法来验证通信协议。我们的方法使用半形式化的协议表示和高效的搜索（前向搜索以及面向故障的测试生成）来分析整个场景范围内的协议，包括外部事件，故障（如数据包丢失，通信链路故障，通信节点中的状态丢失等），以及网络拓扑结构。我们的方法的有效性已通过其应用于各种协议得到证明。在这个项目中，我们将承担三个主要任务。首先，我们将扩展我们以前开发的框架，以计算适当的可靠性指标的现有协议的利益，美国宇航局和HDCCSR社区的价值。其次，我们将开发第一个系统的方法来设计新的协议，满足所需的可靠性标准。最后，我们将使用NASA提供的测试平台，结合NASA和其他HDCCSR研究人员提供的专业知识和软件，对我们的方法进行微调，并证明：（i）确实可以使用系统的、半自动的方法为现有的通信协议计算可靠性度量的精确值，（ii）可以系统地设计新的协议，半自动化的方式，以满足所需的可靠性标准，和（iii）通信协议的可靠性的增强，确实可以显着提高可靠性的许多软件-硬件系统的利益，美国宇航局和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.