| Hi, you discovered why verification is not a panacea. You may prove the most elaborate theorems, but they are meaningless if your specification does not represent the actual system, and an inconsistent set of assumptions is just the most extreme example. Therefore, you need to be suspicious of success and validate your spec as much as you can. Simulation, as well as model checking non-properties and examining the counter-examples are useful for that. Note that this problem applies to both model checking and theorem proving. You should get suspicious if model checking completes very quickly, finds fewer reachable states than you expect, and/or if some actions are taken only rarely or never (TLC provides statistics for this). In theorem proving, get suspicious if a proof obligation that looks complicated is solved quickly and automatically, as it may indicate a contradiction between assumptions – although this is of course not always the case. Regards, Stephan
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1D76B0CC-53E7-4F77-83FD-96FE922D0F9C%40gmail.com. |