The Android programming model presents a system which allows an application to react to various environmental events.  These events can be anything from an mp3 being cached enough to play to a button on the GUI being pressed.  In an app with no concurrency, these events constitute the entire execution of an application when the activity lifecycle events are included.  

When a developer implements an application, they create a series of methods known as callbacks.  On processing an event the framework will execute the appropriate code in addition to invoking a callback if needed.  The Android framework methods invoked by this callback can affect future events by either enabling or disabling them.  This means that a given application cannot observe certain traces of events.  For example if the initial event disables a button then the event which triggers the button’s callback cannot happen afterwards unless another event re enables the button.  These sort of ordering properties are very important when developing applications.  An example would be the MediaPlayer class which will download a song in the background and invoke a callback when it is ready to be played.  Invoking play before it is ready will emit an error.  

Most analyzers manually specify the callback orderings of specific objects such as the Activity lifecycle. This does not account for actions which may enable or disable future events.  In order to overcome this limitation we investigate a framework specification language which captures the behavior of the event callback mechanism.  Using framework specification with the implementation of the application, we can create an automaton that describes the possible orderings of events and their associated callbacks.  Such orderings will be able to catch typestate like errors such as the play button on the android MediaPlayer class being invoked at the wrong time but additionally can augment further static analysis.