2
$\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.

Improve this question
$\endgroup$
1
$\begingroup$

If you want a guarantee, then yes, verification is the only approach. That's pretty much the definition of what verification means.

If you want a heuristic check, there are a number of testing methods based on synthesizing test cases (perhaps based on the DFA) and then checking that the vending machine's actual behavior on those test cases matches your DFA's.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Any references for this? A google search doesn't turn up any obvious contenders. $\endgroup$ – cody Oct 19 '19 at 7:05
  • $\begingroup$ @cody, see grammar induction, Angluin's algorithm, etc. $\endgroup$ – D.W.♦ Oct 19 '19 at 20:25
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.

Improve this answer
$\endgroup$
3
  • $\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 '19 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 '19 at 16:55
  • 1
    $\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 '19 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.