If you want to make money online : Register now

[Solved]: How can I check constraints on my state machine behaviour?

, , No Comments
Problem Detail: 

My background is fairly practical rather than theoretical, so this question may be a bit basic.

I have a state machine with events, and events may optionally trigger action functions to be called as part of the state transition. In practice, actions functions do things like lighting LEDs. The state machine is defined in an in-house domain-specific language, and a tool generates C code from the definition.

I have constraints that need to be satisfied -- eg "when in state A, only LED 1 and 5 should be lit."

What practical techniques are there to check that my state machine design satisfies my constraints?

I considered using Prolog. If I could enter the side-effects of my action functions, the state machine states, and the valid transitions and action functions, I should be able to query whether the constraints hold true -- is this correct?

Are there other frameworks or tools that could be useful in this situation?

Asked By : FusterCluck

Answered By : D.W.

Use a model checker. This is exactly what they're good for. You might look at SPIN and NuSMV as a starting point, but there are many others as well.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/53901

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback