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