Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
    
You might want to read about design by contract. – svick Mar 2 at 15:32
up vote 5 down vote accepted

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.

share|cite|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.