A forum for Spin users
You are not logged in.
Pages: 1
Hello,
I have a basic question. If I want to to verify a model of a simple task, I wrote in promela by simply translating a state machine (suppose a simple string recognition) in a process, how can I model the environment interaction? That is, if I want to express the fact that I have some variable that represent the non-deterministic input to my string-recognition, how can I express this?
My initial idea is to simply put the variables in a process as non-deterministic choices:
active proctype inputs(){
:: skip -> var1 = ENUM1
:: skip -> var1 = ENUM2
:: skip -> var1 = ENUM3
:: skip -> var2 = ENUM1
:: skip -> var2 = ENUM2
[...]
}
This seems to work, but I would like to have confermation about this is the best approach.
If so, I would like to know how to overcome the problem to make "free" variables that are not enumeratives, or that have very large domains.
I apologize for any inaccuracy, but I'm now approaching the model checking techniques.
Thanks to all for the help.
Hello to each forumers,
I'm approaching with formal verification for my master degree thesis. I'm implementing an automatic trasformation from uml state machine to promela process in the scope of model-driven engeenering.
I modelled the state by a global variable "state", and created the aliases for the state by means of "mtype".
I also initialized the variable in a manner like: state = INIT_STATE.
Then I write my process. It is like:
active proctype tsr() {
do
:: (state == INIT_STATE) ->
// do-things
:: (state == T01) ->
// do-thing
etc.
}
So it happens to me that when I try interactive simulation, spin asks to choice the value of the state as if it were a non-deterministic choice.
But I initialized the state variable for avoid this non-determinism.
So what is my (conceptual, i think) error?
Thanks in advance for help.
Alessandro Ranieri
Pages: 1