(Generally) How to specify asynchronous action with side effects using logic equations

Question

Say you have this function call sequence:

function all() {
  fn1()
  fn2()
  fn3()
}

And say that fn2 was asynchronous and caused all kinds of side effects:

var globalPacketCounter = 0

function fn2() {
  var httpRequest = ...
  httpRequest.on('data', function(){
    globalPacketCounter++
  })
  drawGraphicsToDisplay()
  ...
}

Something complicated and with unknown implementation, though you can probe it to determine the types of behavior it has, and read docs, etc.

I'm wondering, generally speaking, what you can do to incorporate this into a model checking or symbolic evaluation system, or other verification system like Hoare logic or something. I would like to do this:

all() =
  /\ fn1() in state 1
  /\ fn2() in state 2
  /\ fn3() in state 3
  /\ complete = true in state 4

Some sort of logical statement. The question is (partially) if this is a valid approach; that is, treating the fn2() as a single step in a logic equation. The main part of the question though is how to generally do this. I would like to basically treat everything as logic functions but am not sure how to apply it to the "async with side effects" case.

Answer 1

The way to incorporate it in a model depends on (a) what aspects of system behavior you want the model to capture, (b) what properties you want to verify of the system, and (c) what kind of expressivity the model checker framework provides.

In other words, there's no one way to model systems. One can build multiple models of the same system, each focusing on different aspects of the system, or modelling it to a different level of abstraction/precision.

For instance, in something based on pi calculus, one possible way to model asynchronous operations is as spawning a separate process to perform that stuff concurrently.

Answer 2

One way to model your example is through program graphs. (See chapter 2 in Principles of Model Checking.) What you can do is model all() as one program, which synchronizes on action 'data' with another program that runs concurrently to all(), let's call it listen(). listen() will have an initial state where it waits until it can synchronize with the all() on action 'data'.

Once you have these two models (or more for bigger examples) you can interleave them, which is a construction that contains all the possible states. Program graph interleaving also preserves shared variables (so globalPacketCounter will be updated correctly) unlike interleaving on transition systems. Though I would be careful about them, since atomicity is not implicit in the models. You can read more about critical actions in section 2.2.2. of the book.

After interleaving of PGs you construct a transition system, which you can transform to a logical equation. And there you have it.