A forum for Spin users

You are not logged in.

#1 2019-08-06 09:22:12

Registered: 2019-07-13
Posts: 1

Generating System Model using Promela

In last semester I took Model checking course and decided to pursue my career in the field of Formal Verification.
Till now, I covered the internal working of Spin model checker from source code, especially the complete process of
Verification  Mode. I solved all small examples given for different keywords in "http://spinroot.com/spin/Man/promela.html"
and other tutorials from spinroot.com. But I don't know any resource which tells how to extract a model from a
given system and write it in Promela(a complete step by step example). All examples I have found already have the model
written in Promela. Can anyone please provide a complete example or link to understand the whole procedure. Thanks!


#2 2019-08-06 18:18:07

Registered: 2010-11-18
Posts: 654

Re: Generating System Model using Promela

the distribution of modex (spin's model extractor for c-code) contains example files in c for which the tool can extract spin models -- but you can also look at that c-code yourself and manually build models, as an exercise


Board footer

Powered by FluxBB