Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-01 11:23:27

shanky06
Member
Registered: 2012-04-01
Posts: 4

SPIN protocol simulations !!

Hi

I am working on a project related to Wireless Sensor Networks and my study is based on protocols like SPIN and LEACH.
I am now working on SPIN and i need to know how can i get started with it.Which OS,Linux or Unix ? Which Network Simulator supports SPIN? I have read that ns-2.1b5 supports the code extension for SPIN but i think it outdated and not supported anymore?
Where can i find the latest code extensions for SPIN and which network simulator supports it?
If anyone can provide me the guideline for working on SPIN please help me out.

Regards
shanky06

Offline

#2 2012-04-01 22:30:47

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: SPIN protocol simulations !!

which OS: any
which network simulator: none
ns-2.1b5: is an application (a protocol) that Spin could be applied to, and possibly has been applied to
spin source code: http://spinroot.com/spin/Src
spin executables: http://spinroot.com/spin/Bin
spin tutorials etc: http://spinroot.com/spin/Man
spin books and papers: http://spinroot.com/

Offline

#3 2012-04-02 10:44:26

shanky06
Member
Registered: 2012-04-01
Posts: 4

Re: SPIN protocol simulations !!

Thank you so much for the reply but i have a few doubts.
No network simulator implements SPIN? How can i then get the results i want such as throughput , latency ??
Will it work on ubuntu version 10.10 ?? how do i go about installing or implementing it?
So do i just run the code on the terminal and i would get the results is it ??

Regards
shanky06

Offline

#4 2012-04-02 15:57:03

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: SPIN protocol simulations !!

Throughput and latency are not quantities that Spin computes.
Spin is a logic model checker -- see http://spinroot.com/ for a general description of what the tool is for.
It works on any OS, including any version of Ubuntu.
To install it you follow the instructions that are given on the download page -- and yes, you just run it from a console window and get the results.

Offline

#5 2012-04-02 18:28:21

shanky06
Member
Registered: 2012-04-01
Posts: 4

Re: SPIN protocol simulations !!

thank you spinroot..i shall try out and post the results.

Regards

Offline

#6 2012-04-04 14:25:09

shanky06
Member
Registered: 2012-04-01
Posts: 4

Re: SPIN protocol simulations !!

Hi spinroot ,
I have another doubt ..i have gone through the pages you referred to me and i am still a little confused..Can you just list out 2-3 quantities which SPIN (Sensor protocol for Information via Negotiation) calculates.I mean if it does not give the throughput,latency as the output then what other quantity does it calculate?
Network Lifetime etc?

Thanks again

Offline

#7 2012-04-05 14:43:35

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: SPIN protocol simulations !!

Typical problems solvable by SPIN are the following: Is a desired property (such as freedom of deadlock, a variable is always smaller than a limit) always satisfied by the protocol? Can the protocol eventually finish the job? If property A holds, will property B eventually be also satisfied? These are just a fraction of the rich problems to be solved by SPIN.

SPIN doesn't naturally support numerical solution to the problem. It cannot precisely calculate the worst execution time of a program, neither can it predict the maximal throughput of the network. These problems can only be solved with special tricks of using SPIN in a smart way. For example, if ones wants to find the worst execution time, one must estimate it first (say T) and then ask SPIN "Is it true that the program always finish within T?" If SPIN tells you yes, then the worst execution time must be something less than or equal to T. On the contrary, if SPIN tells you no, the worst execution time must be something larger than T. Then you modify your estimate and give the new value to SPIN. After a few iterations, you will get the correct answer.

This iterative process may even be automated.

Offline

#8 2012-04-06 00:11:07

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: SPIN protocol simulations !!

> shanky06 wrote:

> Hi spinroot ,
I have another doubt ..i have gone through the pages you referred to me and i am still a little confused..Can you just list out 2-3 quantities which SPIN (Sensor protocol for Information via Negotiation) calculates.I mean if it does not give the throughput,latency as the output then what other quantity does it calculate?
Network Lifetime etc?

I think we've found the problem:  "SPIN" on this forum and website is not an acronym for "Sensor protocol for Information via Negotiation"
Spin is a logic model checking tool for verifying asynchronous process systems.
SPIN stands for "Simple Promela Interpreter" and "Promela" stands for "Process Meta Language"
So I think you hit the wrong forum!

Offline

Board footer

Powered by FluxBB