Spinroot

A forum for Spin users

You are not logged in.

#1 2011-03-09 10:56:56

ines.md
Member
Registered: 2011-03-08
Posts: 7

Spin verification cycle

Good morning,
Does the spin verify cycles, ie does it verify Termination property in case of cycles?
And can it veify the Livelock property?

Thanks

Offline

#2 2011-03-10 01:53:09

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

Re: Spin verification cycle

Yes, Spin can find cycles. It can verify arbitrary liveness properties and LTL.
More precisely, it can verify any omega-regular property. LTL defines only a subset of the omega-regular properties.

Offline

#3 2011-03-14 12:05:08

ines.md
Member
Registered: 2011-03-08
Posts: 7

Re: Spin verification cycle

So Can it also check the properties of Livelock in the case of cycles?

Offline

#4 2011-03-15 16:16:40

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

Re: Spin verification cycle

yes

Offline

#5 2011-03-15 18:18:52

ines.md
Member
Registered: 2011-03-08
Posts: 7

Re: Spin verification cycle

sorry but what i want to know is, if just to check the "Non-progress" property and verify my model that means the verification of the "Livelock" property in the case of cycle??? or i have to enter a LTL property that exprime the Livelock of my model and then verify?

An other question please: what's the difference of "Acceptance" and "Non-progress" property? are used both to verify the correctness of models in the case of cycle?does "Acceptance" used to verify cyclic models but here we accept cycle and "Non-progress" used to verify cyclic models but spin should takes into consideration the non-progress cycle or to avoid its???

thanks

Offline

#6 2011-03-16 02:57:19

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

Re: Spin verification cycle

there are no quick one sentence answers to the questions you ask
please study the tutorial material or read the textbook that explains the context for logic model checking, and you'll understand much better how things work

a non-progress property is a special type of an acceptance property, where acceptance refers to Buchi acceptance (a form of omega acceptance).
ltl properties can express a subclass of properties that can be checked with Buchi automata.

your questions go deeper though and i recommend that you go through the material on the website that was prepared to give you a better insight in the verification process

Offline

Board footer

Powered by FluxBB