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.