Suppose I have modeled a deterministic finite automaton of my system. How can I check if the traces generated by this system, actually represent the model I had in mind?
For example, say I have DFA A which models a vending machine. To ensure I did not model any wrong transitions, is coming up with (safety/liveness) specifications and performing verification the only method I can follow to ensure my model is correct? Many thanks.