A visual semantics for communication protocols

通信协议使多台计算机能够相互交互。 这些协议的安全关键应用，例如管理飞机中嵌入式组件通信的应用，要求在所有输入条件下对其性能具有极高的置信度。 自动推理工具，如模型检查器，可以执行这种分析，如果发现研究中的协议有错误，报告错误的确切性质和原因，以帮助重新设计协议。 这种类型的推理要求协议以数学上精确的形式表示，这有助于自动推理。 此外，仅当协议描述具有可管理的大小时才可以执行分析。这个项目将开发可视化的，直接的符号来描述通信协议的行为。 精确和直观的可视化符号将帮助开发人员建模和分析所研究的协议。由于协议的巨大规模，需要自动推理机来帮助设计人员管理其分析中固有的复杂性。基于这些可视化符号，自动推理工具，如模型检查器，将被开发来分析下一代通信协议。最终，这些工具将有助于为我们每天使用的电话系统和互联网等基本通信工具提供服务保障。

Communication protocols enable several computers to interact with each other. Safety critical applications of these protocols, such as those governing the communications of embeded components in aircraft, demand an exceptionally high degree of confidence in their performance under all input conditions. Automated reasoning tools, such as model checkers, can perform this analysis and, if a protocol under study is found to have a bug, report on the exact nature and cause of the bug in order to help redesign the protocol. This type of reasoning requires that the protocols be expressed in a mathematically precise formalism that lends itself to automated reasoning. Further, the anlysis can be carried out only when the protocol description is of a managable size. This project will develop visual, straightforward notations for describing the behavior of communications protocols. Visual notations that are both precise and intuitive will help developers in modeling and analyzing the protocols under study. Due to the enormous size of the protocols, automated reasoners are needed to help designers manage the complexities inherent in their analysis. Based on these visual notations, automated reasoning tools, such as model checkers, will be developed to analyze next generation communication protocols. Ultimately, these tools will help deliver service guarantees for the essential communications tools such as phone systems and the Internet, that we use every day.