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.