A forum for Spin users
You are not logged in.
Pages: 1
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
Pages: 1