Spinroot

aleander

Member

Registered: 2013-01-25

Posts: 3

model the environment interactions

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.

Last edited by aleander (2013-02-07 20:20:34)

spinroot

forum

Registered: 2010-11-18

Posts: 704

Website

Re: model the environment interactions

That's a reasonable way to do it. (you don't need the skips before the assignments though)
Another way would be to add an explicit process the model the environment.
The model will have to remain finite state though, so you may want to avoid large domains for nondeterministic assignments.