Verifying network protocols using temporal logic
Verifying network protocols using temporal logic(1980)
摘要
Programs that implement computer communications protocols can exhibit extremely complicated behavior, and neither informal reasoning nor testing is reliable enough to establish their correctness. In this paper we discuss the application of program verification techniques to protocols. This approach is more reliable than informal reasoning, but has the advantage over formal reasoning based on finite-state models that the complexity of the proof does not grow unmanageably as the size of the program increases. Certain tools of concurrent program verification that are especially useful for protocols are presented: history variables that record sequences of input and output values, temporal logic for expressing properties that must hold in a future system state (such as eventual receipt of a message), and module specification and composition rules. The use of these techniques is illustrated by verifying a simple data transfer protocol from the literature.
更多查看译文
关键词
temporal logic,eventual receipt,concurrent program verification,program increase,informal reasoning,program verification technique,verifying network protocol,complicated behavior,certain tool,composition rule,formal reasoning,computer communications protocol
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络