Verification of Simulation Models of Network Protocols Using State Space Exploration and Protocol-Specific Properties

摘要: Verification and Validation (VV i.e., a safety property. In this paper, we elaborate on the state space exploration framework in J-Sim demonstrate its usefulness effectiveness verifying complicated simulation models. Specifically, verify models of two widely used fairly complex network protocols: Ad-Hoc On-Demand Distance Vector (AODV) routing protocol for wireless ad hoc networks directed diffusion data dissemination sensor networks. To enable verification these models, make use structural properties underlying along orthogonal dimensions; first uses non-trivial relation to prune states be searched, second is ranking that determines whether “better than” another order implementation best-first search (BeFS). We also develop protocol-specific heuristics guide towards finding assertion violations less time. particular, report findings how devise good routing/data protocols similar AODV diffusion. show time needed find an violation by our comparable Java PathFinder (JPF), state-of-the-art model checker programs.1