Sciweavers

Share
CONCUR
2009
Springer

Query-Based Model Checking of Ad Hoc Network Protocols

9 years 4 months ago
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...
Anu Singh, C. R. Ramakrishnan, Scott A. Smolka
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CONCUR
Authors Anu Singh, C. R. Ramakrishnan, Scott A. Smolka
Comments (0)
books