# How Model Checking works with User Interaction

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).

• 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. – Derek Elkins Jun 29 '18 at 5:07