So with Model Checking you have a specification and the model checker automatically goes through your program's states and checks if it matches the specification. What I don't understand is where testing fits it. So typically it is described that if Model Checking finds an error, it will generate a test case to demonstrate the error. That makes sense, this allows you to iterate on a solution until finally the test passes.

My first question then is, assuming you get that test to pass (the test generated by the model checker), I'm wondering what you now do with the test:

  1. Throw it away, it's no longer needed.
  2. Save it to test periodically in a regression test run. (But seems like the model checker will catch these anyways, so not sure if it's necessary, seems like duplication.)
  3. Somehow have a suite of tests alongside the model checker / specification that you always run because the model checker can't handle those.

That brings up the second part of the question which is, the kinds of things you write tests for if you have model checking. If that is too broad then just knowing the workflow for dealing with model-checker-generated tests would be useful.

  • Could you share what model checker and language you are using? In my experience, people in production systems only use model checking to verify specifications are correct, not that code matches specifications. – Hovercouch Jul 28 '18 at 21:59

Your Answer

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

Browse other questions tagged or ask your own question.