Spinroot

Shafaqat

Member

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!

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

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