Spinroot

A forum for Spin users

You are not logged in.

#1 2012-02-15 00:28:23

amrad
Member
Registered: 2012-02-15
Posts: 4

About SPIN

Hi all,

i would like to use SPIN to verify some LTL proprieties and validation.
My question is about the input of SPIN. i know that the input is a PROMELA language. Can i use the ARINCTester to translate an XML file to Promela.

Also, should i write only the proprieties to verify or  there is a program?
Can i found some simple exercises  of SPIN or some steps about how to use SPIN because i am new in the model checking.

thank you in advance.

Offline

#2 2012-02-15 06:00:50

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

Re: About SPIN

check out the tutorials on http://spinroot.com/spin/Man

Offline

Board footer

Powered by FluxBB