How can I check constraints on my state machine behaviour?

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?

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.

StackExchange Computer Science Q#53901, answer score: 5