Combining SPIN with ns-2 for Protocol Optimization

In the field of communication networks, protocol engineers usually employ several tools focused on specific kinds of analysis, such as performance or correctness. This paper presents an approach to integrate the analysis capabilities of the Spin model checker and the ns-2 network simulator into a single framework. In particular, we use the verification capabilities of Spin to control the execution of ns-2. The traffic-oriented model of the protocols is managed by ns-2, while SPIN automatically generates the most suitable configurations of each ns-2 run in order to meet some designer requirements. These requirements are specified with assertions and with an annotated temporal logic that can be translated into Spin s B¨uchi automata. Spin verification algorithms help us to automatically discard those ns-2 configurations and simulations that do not satisfy the expected requirements. With this approach we can automatically obtain the suitable values of parameters like buffer size,...

• Type: Journal
• Year: 2010
• Where: SPIN
• Authors: Pedro Merino, Alberto Salmeron
• Keywords: Ns-2, Spin, SPIN 2010, Temporal Logic, Theoretical Computer Science