1
$\begingroup$

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.

|cite|improve this question
$\endgroup$
0
$\begingroup$

For correctness proofs, you have to use induction. See here, correctness proof of DFA. For safety checking, you can check for words which belong to the language of the DFA and run it to see of it gets accepted. Also, check for words which do not belong to the language of the DFA and make sure they get rejected.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ The 'words' you use here (which is standard CS terminology), are what the question refers to as 'traces'. I'm not sure how the sort of correctness proof you link to helps, could you clarify that? $\endgroup$ – Discrete lizard♦ Apr 20 at 16:53
  • $\begingroup$ The link shows an approach to prove the correctness of a DFA. As the inductive step depends on the language, It is hard to generalize for all DFAs. The second part is just a manual safety checking that the DFA works well for the inputs. $\endgroup$ – SiluPanda Apr 20 at 16:55
  • $\begingroup$ You have to be clear what 'correctness' means here. In your example, what you prove is the that the DFA accepts some language. I highly doubt the system referred to in the question is defined by a clear language description, so I don't see what use this particular notion of correctness would have here. $\endgroup$ – Discrete lizard♦ Apr 20 at 16:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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