1
$\begingroup$

In order to understand how to apply Model Checking, I am wondering how to apply it to a pseudo-realistic async program.

Say I have the following pseudocode:

var array = []

window.onclick = a

function a() {
  setTimeout(b, 10)
}

function b() {
  setTimeout(c, 100)
}

function c() {
  var data = new Data(1)
  array.push(data)
}

function Data(integer) {
  this.integer = integer
}

The program asynchronously does a() -> b() -> c() on click and constructs a new Data object.

Say I have a specification that says "The program will eventually create a Data object on click within 200ms". Wondering what the Model Checker does to prove that this is correct in the program.

So first I rewrite my program as a state machine.

  • State start
    • Transition to State idle.
  • State idle
    • Transition click to State a.
  • State a
    • Transition setTimeout to State b.
  • State b
    • Transition setTimeout to State c.
  • State c
    • Transition "function" to State d (does var data = new Data(1); array.push(data)).
  • State d
    • Transition to State idle

Then the model checker starts at the start state and needs a "click" event to trigger going to state a. Wondering what the model checker path/trace will look like going from start to state d. That will help in understanding how to apply model checking. I don't see how to provide the click event to the model checker or how it should prove the Data statement. It seems like there needs to be some sort of testing/input generation going on but not quite sure (like for generating a fake click event for example).

$\endgroup$
  • 1
    $\begingroup$ Unless you run a model checker to completion, which is usually infeasible, a model checker doesn't prove the usual sorts of statements its applied to, e.g. safety statements that say that some invariant always holds. A model checker is not usually used to prove things. It is used like testing. If it finds a counter-model, you have a problem, but if it doesn't then you don't know whether the code is right or not. $\endgroup$ – Derek Elkins Jun 29 '18 at 5:07

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.