Query-Based Model Checking of Ad Hoc Network Protocols

Abstract. A prominent source of complexity in the verification of ad hoc network (AHN) protocols is the fact that the number of network topologies grows exponentially with the square of the number of nodes. To combat this instance explosion problem, we present a query-based verification framework for AHN protocols that utilizes symbolic reachability analysis. Specifically we consider AHN nodes of the form P : I, where P is a process and I is an interface: a set of groups, where each group represents a multicast port. Two processes can communicate if their interfaces share a common group. To achieve a symbolic representation of network topologies, we treat process interfaces as variables and introduce a constraint language for representing topologies. Terms of the language are simply conjunctions of connection and disconnection constraints of the form conn(Ji, Jj) and dconn(Ji, Jj ), where Ji and Jj are interface variables. Our symbolic reachability algorithm explores the symbolic st...

• Type: Conference
• Year: 2009
• Where: CONCUR
• Authors: Anu Singh, C. R. Ramakrishnan, Scott A. Smolka
• Keywords: CONCUR 2009, Distributed And Parallel Computing, Network Topologies, Symbolic Reachability, Symbolic Reachability Analysis