Software Model Checking of UDP-based Distributed Applications
Computing and Networking(2015)
摘要
We extend exhaustive verification of networked applications to applications using the User Datagram Protocol (UDP). UDP maximizes performance by omitting flow control and connection handling. High-performance services often offer a UDP mode in which they handle connections internally for optimal throughput. However, because UDP is unreliable (packets are subject to loss, duplication, and reordering), verification of UDP-based applications becomes an issue. Even though unreliable behavior occurs only rarely during testing, it often appears in a production environment due to a larger number of concurrent network accesses. Our tool systematically tests UDP-based applications by producing packet loss, duplication, and reordering for each packet. It is built on top of net-Rio cache for the Java Path Finder model checker. We have evaluated the performance of our tool in a multi-threaded client/server application and detected incorrectly handled packet duplicates in a file transfer client.
更多查看译文
关键词
client-server systems,formal verification,transport protocols,udp-based distributed application,exhaustive verification,file transfer client,high-performance services,multithreaded client-server application,packet duplication,packet loss,packet reordering,software model checking,user datagram protocol,java path finder,testing of distributed systems,unreliable network io
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要