Abstracting Event-Driven Systems with Lifestate Rules
Shawn Meier
Aleksandar Chakarov
Maxwell Russek
Sergio Mover
Bor-Yuh Evan Chang

arXiv:1701.00161v1 [cs.PL] 31 Dec 2016

University of Colorado Boulder
{shawn.meier, aleksandar.chakarov, maxwell.russek, sergio.mover, evan.chang}@colorado.edu

Abstract
We present lifestate rules—an approach for abstracting
event-driven object protocols. Developing applications
against event-driven software frameworks is notoriously
difficult. One reason why is that to create functioning
applications, developers must know about and understand the complex protocols that abstract the internal
behavior of the framework. Such protocols intertwine the
proper registering of callbacks to receive control from the
framework with appropriate application programming
interface (API) calls to delegate back to it. Lifestate rules
unify lifecycle and typestate constraints in one common
specification language. Our primary contribution is a
model of event-driven systems λlife from which lifestate
rules can be derived. We then apply specification mining
techniques to learn lifestate specifications for Android
framework types. In the end, our implementation is able
to find several rules that characterize actual behavior of
the Android framework.

1.

l.onClick(b)
b.onDraw()

b.enable()

b.enable()

b.disable()
b.disable()

l.onClick(b)
(a) Multi-object lifecycle

(b) Mixed lifecycle-typestate

b.disable()
b.enable()

b.disable()

b.onDraw()

b.enable()
b.disable()

b.onDraw()

b.enable()

b.disable()

b.enable()
l.onClick(b)
(c) Product of (a) and (b)

Figure 1. Event-driven object protocols are complex.

Introduction

complete. Because lifecycle constraints are so central
to implementing apps, they are typically discussed in
the framework documentation, but they are incomplete
enough that developers spend considerable manual effort
to derive more complete specifications [30].
To get a sense for the complexity of event-driven
object protocols, consider the automaton-based specifications shown in Figure 1.The meaning of such a
specification is that execution traces (projected on to
the actions of interest) must be words accepted by the
automaton. In Figure 1a, we describe a portion of a lifecycle specification for a protocol between a button object
b and its click-listener l. This automaton states that a
b.onDraw() callback notification happens before any
l.onClick(b) callback invocations. This specification
is a multi-object lifecycle constraint because it orders
callbacks on objects b and l.
In Figure 1b, we show another important property of
buttons and their click-listeners: a button can be enabled
or disabled via API calls b.enable() and b.disable(),
respectively. When button b is enabled (the upper state),

We consider the problem of specifying and mining the object protocols used by event-driven software frameworks.
Programming against event-driven frameworks is hard.
In such frameworks, programmers develop client applications (apps) against the framework by implementing callback interfaces that enable the application to be notified
when an event managed by the framework occurs (e.g.,
a user-interface (UI) button is pressed). The app may
then delegate back to the framework through method
calls to the application programming interface (API)
(e.g., to direct a change in the UI display). To develop
working apps, the application programmer must understand the complex object protocols implemented by the
event-driven framework. For example, the framework
may guarantee particular ordering constraints on callback invocations (known as lifecycle constraints), and
the application programmer may have to respect particular orderings of API calls (i.e., typestate constraints).
Unfortunately, such protocol specifications are complex to describe and maintain—and almost always in1

• We formalize a concrete semantics for event-driven

the click-listener l may receive the l.onClick(b) callback notification. Through an API call to b.disable(),
button b becomes disabled. When button b is disabled
(the lower state), the click-listener l can no longer receive
l.onClick(b) notifications. This specification mixes a
lifecycle (or callback-ordering) constraint with a typestate (or API call-ordering) constraint.
We call API calls into the framework, callins, to
clearly contrast them with callbacks that are calls back
from the framework. The specification in Figure 1b
mixes two kinds of invocations: (1) events labeled by
the callbacks they invoke to notify the app (written
slanted) and (2) callins that the app invokes to change
the state of the framework (written upright).
From just the examples in Figure 1, we see that the
specification space is rich and complex with multiple
interacting objects over callbacks and callins. Worse, the
composition of the onDraw-before-onClick specification
from (a) and the enable-disable-onClick specification
from (b) is the product automaton shown in (c). In this
product automaton, the left states are where button b
is enabled versus the right states where b is disabled,
and the upper states are where button b has yet to
be drawn versus the lower states are where b has been
drawn. While automata are descriptive and natural, the
key observation of this paper is that automata are more
precise than necessary or desired.
Thus, we take a departure from traditional automaton specifications and define a more abstract specification language consisting of lifestate rules that captures
the critical lifecycle and typestate constraints without
representing them as automata. We shall see that this
specification language is more compact than automata
and exposes lifecycle and typestate constraints as duals. At a high level, lifestate rules focus on changes in
the internal, hidden state of the event-driven framework.
For example, the enable-disable-onClick specification
from Figure 1b can be summarized as the following rules:
b.enable()
b.disable()

systems using an abstract machine model λlife that
captures an appropriate model of the internal, hidden
state of the framework (section 3). We introduce the
notion “allowedness” for API callins, which we shall
see is parallel to “enabledness” for events.
• We define a language for lifestate rules, which incorpo-

rates mixed lifecycle-typestate constraints (section 4).
• We introduce callback-driven trace slicing, a form

of trace slicing [14] adapted to events and callbacks
(section 5). The λlife model and this trace slicing
algorithm is the basis for our dynamic analysis tool,
DroidLife, that records events, callbacks, and callins
in running Android applications.
• We apply specification mining techniques to derive

lifestate specifications (section 6). In particular, we
apply unsupervised automata-based learning techniques based on probabilistic finite state automata
and hidden Markov models. We also develop a direct lifestate mining technique based on propositional
model counting (]SAT). The most significant challenge with lifestate mining is that the enables, disables,
allows, and disallows that explain callback and callin
invocations are not observable in concrete executions.
• We empirically evaluate our mining algorithms on 133

traces from a corpus of 1,909 Android apps (section 7).
Our results show that we can in fact learn several rules
corresponding to actual Android behavior and one of
which that was not in the Android documentation.

2.

Overview

In this section, we motivate the challenges in specifying
and mining event-driven object protocols and then
exhibit how our approach models event-driven systems
to mine lifestate rules about the Android framework.
We will show with our running example in Figure 2 that reasoning about the correctness of apps
requires a comprehensive understanding of the lifestate rules of various Android framework components.
In particular, the call marked with B can throw an
IllegalStateException. This code is correct, but understanding why requires a specification of subtle relationships between the various callins and the events
that trigger the callbacks. We will also see that a slight
change of this code makes it buggy.

enables l.onClick(b) for some l
disables l.onClick(b) for some l

The first rule says that whenever the invocation
b.enable() fires, the state of the framework changes
to enable the event that invokes the l.onClick(b) callback, and the second rule says when b.disable() fires,
the state changes to disable the event that invokes
l.onClick(b). These rules do not enumerate the explicit
invocation orders as in the automaton from Figure 1b.
Having defined lifestate rules for event-driven object
protocols, we investigate specification mining techniques
from dynamic traces of apps using a framework. To
address the technical challenges to this end, we make
the following contributions:

Lifestate Specification. Android is a prominent example of an event-driven framework that dispatches
a multitude of events (e.g., from user interaction or
sensors). An app gets notified about events by implementing callback interfaces that may then delegate back
to the framework through the framework’s callin interface. We consider an event-driven object protocol to be
the rules governing the use of an interface consisting of
2

callbacks and callins. Unfortunately, the protocol rules
are determined by the complex, internal behavior of the
framework, which becomes a major source of confusion
for app developers and thus of defects in apps.
To see this complexity, consider the code shown in
Figure 2. The app performs a time consuming operation (removing feeds) when the user clicks the button
b. The operation is performed asynchronously using
AsyncTask to not block the UI thread. Figure 2b shows
an execution trace of the app. Execution time flows
downwards. A box surrounds the callback and callin
invocations that happen as the result of processing of a
particular event. First event Create invokes the callback
(a:Activity).onCreate() for the object a. In this case,
object a has dynamic type MainActivity; for reasons we
will discuss below, we label the object with its most precise supertype that is a framework type. In the onCreate
callback, the code then invokes a callin for the AsyncTask
constructor (i.e., (t1:AsyncTask).<init>()) and then
the callin for setOnClickListener following the app
code at line 5. Then, the trace shows the execution of
other two events, Click, with the callback onClick, and
PostExecute, with the callback onPostExecute.
Figure 2b also depicts the back and forth flow of
control between framework and app code. The boxes
along the lines show the lifetime of activations. In
particular, we see that we can define a callback invocation
as the invocation that transfers control from framework
code to app code (arrows to the right), while a callin
is the reverse (i.e., an invocation that transfers control
from app code to framework). The difficulty in reasoning
about the code in Figure 2a is that framework behavior
that governs the possible control flow shown in Figure 2b
is obfuscated in the code.
Our running example is inspired by an actual issue in AntennaPod [1] a podcast manager for Android
with 100,000–500,000 installs from the Google Play
Store(a similar issue appears in the Facebook SDK
for Android [2]). The potential bug is that the callin
AsyncTask.execute, called via remover.execute() (line 7),
can throw an IllegalStateException.
In the example the execute call happens whenever
the user clicks button b, which in turn triggers the
event that dispatches to the OnClickListener.onClick
callback on the click-listener (set on line 5). This code
is indeed safe (i.e., does not throw the exception) because the developer enforces that the execute method
on FeedRemover is only called once. This property is
enforced by the disabling and enabling of button b
in onClick and in onPostExecute, respectively. Buttons in Android are disabled and enabled via calls to
setEnabled(false) and setEnabled(true), respectively
(corresponding to disable and enable in section 1).

3

class FeedRemover extends AsyncTask {

MainActivity a; Button b;
void doInBackground() { . . . remove feed . . . }
void onPostExecute() {
a.remover = new FeedRemover(a, b);
b.setEnabled(true);
}

1
2

}
class MainActivity extends Activity {

FeedRemover remover;
void onCreate() {
Button b = . . .;
remover = new FeedRemover(this, b);
b.setOnClickListener(new OnClickListener() {
void onClick(View v) {
b.setEnabled(false);
remover.execute();
B
}
});
}

3
4
5
6
7

}
(a) The call remover.execute() on line 7 (marked with B) can
throw an IllegalStateException if the remover task is already
running. This execute call happens whenever the user clicks button
b. This code is indeed safe because the developer enforces that
only one instance of FeedRemover is ever executing through the
disabling and enabling of the button on lines 6 and 2, respectively
(shown with dashed underline).
Framework

App

Create
(a:Activity).onCreate()
(t1:AsyncTask).<init>()
(b:Button).setOnClickListener(l:OnClickListener)

4
5

Click
(l:OnClickListener).onClick(b:Button)
(b:Button).setEnabled(false)

6

(t1:AsyncTask).execute()
7

PostExecute
(t1:AsyncTask).onPostExecute()
(t2:AsyncTask).<init>()
1

(b:Button).setEnabled(true)

2

(b) A DroidLife trace recorded dynamically. Each box is the
processing of an event. Callbacks are depicted as arrows to the
right from framework to app code; callins are arrows to the left,
which are labeled with the corresponding program location from
Figure 2a.

Figure 2. An example Android app whose safety depends on understanding the lifestate rules of two Android
framework components AsyncTask and Button.

(t:AsyncTask).execute()

small caps) and associate events with the callback(s)
they trigger (written EventonCallback()). Finally,
the last rule states that the asynchronous task constructor (t:AsyncTask).<init>() allows the t.execute()
callin. We define and discuss the formal semantics of
lifestate specifications in section 4.
We argue that specifications describing the enablingdisabling of events and the allowing-disallowing of callins
are central to event-driven object protocols. The specifications capture the relations that informally say, “When
a particular method invocation happens, the state of
the framework changes to enable or disable an event
or to allow or disallow a callin.” We unify the notions
of events and callins by introducing the term message.
To reason about lifestate specifications, we formalize an
abstraction of event-driven frameworks, called λlife , that
captures the internal state consisting of enabled and
allowed messages in section 3.

9 ci t.execute()

(b:Button).setEnabled(false)
9 evt Click(l:OnClickListener).onClick(b)
(t:AsyncTask).execute()
→ evt PostExecutet.onPostExecute()
(b:Button).setEnabled(true)
→ evt Click(l:OnClickListener).onClick(b)
(t:AsyncTask).<init>()
→ ci t.execute()

Figure 3. Some lifestate rules for AsyncTask and Button.
The first rule specifies a typestate property, while the
others are required to reason about the safety of the call
to remover.execute() in Figure 2a.
To see why this button disabling and enabling
enforces the single-executing-instance property, the
developer needs to know the interactions between
AsyncTasks, Buttons, and OnClickListeners in the Android
framework. Only with an understanding of the framework do we see that the call to b.setEnabled(false)
(line 6) disables the event that could trigger the
onClick callback (which calls the potentially problematic remover.execute()). Button b (and thus
the click event) can be enabled inside the callback
onPostExecute (line 2), but again with an understanding of the framework, we see that onPostExecute is
triggered by a post-execute event, which is in turn enabled by the call to remover.execute() (line 7). When
this happens, remover is set to a newly-allocated instance of FeedRemover (line 1), which allows for the
execute callin to be executed safely.
Without the calls to setEnabled that disables and
enables button b, (on lines 6 and 2, respectively), the app
is buggy because the user can click the button a second
time, causing a second call to remover.execute() on
the same instance of FeedRemover.
The “understanding” of the Android framework that
is necessary to reason about the code in Figure 2a
is precisely what we seek to capture with lifestate
specifications. In Figure 3, we sketch the lifestate rules
needed to reason about our running example. The first
rule, (t:AsyncTask).execute()9 ci t.execute() says
that when (t:AsyncTask).execute() is invoked for an
object t of type AsyncTask, the execute callin on t is
disallowed. We use the terms allowed and disallowed
to refer the state of callins; these terms are parallel to
enabled and disabled for the state of events. Overall, this
rule specifies that it is erroneous to call execute twice
(without something else that re-allows it).
The subsequent three rules specify disabling (written 9 evt) and enabling (written → evt) events (e.g.
setEnabled enables the onClick callback). To make
clear that the enabled-disabled state refers to events,
we give names to events, such as Click (written in

Callback-Driven Trace Slicing and Lifestate Mining. We cannot actually observe the abstraction of
the internal framework state of a running Android app.
Instead, we can only observe the sequence of method
invocations. We use the operational semantics of λlife
to derive an instrumented semantics that captures the
behavior that we can observe: messages classified into
event, callback, callin, or internal invocations. This instrumented semantics specifies the recording needed to
produce traces like the one shown in Figure 2b and is
implemented in a tool called DroidLife.
We are interested in rules about the interactions between events and callins on framework objects. To collect
traces across multiple executions, we apply the standard
type abstraction to concrete objects, resulting in an
abstract, signature message like AsyncTask.execute().
To obtain relevant lifestate rules and improve the
feasibility of mining, we slice recorded traces into subtraces that group together related method calls. Our
approach is roughly to slice a recorded trace into subtraces that collect method invocations whose arguments
share a particular concrete object, similar to Pradel
et al. [32]. However, we face the additional difficulty that
an event message is not directly a method invocation
and the relevant framework object of the event is
typically hidden in the internal state of the message.
Our insight for identifying relevant event messages
is that an event should eventually trigger a callback
where the relevant framework object is also argument
to the callback. Thus, our callback-driven trace slicing
approach determines the relevance of an event message
m based on the arguments to the callback(s) that m
eventually triggers. For example, in our trace slice
for the concrete object t1:AsyncTask, the slice includes
the PostExecute event because it eventually triggers
the callback t1.onPostExecute() and so the type4

e ∈ Expr ::= v | · · · | if v then e1 else e2
| bind v1 v2
| allow v | disallow v | invoke v1 v2
| enable v | disable v
| force m
| let x = e1 in e2
λ ::= fung x in e
g ::= app | fwk
v ∈ Val ::= x | me | · · · | λ | a | κ | h | ()

application. We also assume that there are some heap
operations of interest for manipulating a global store
ρ. Events occur non-deterministically and return to the
main event loop, so events must communicate through
the shared, global heap.
The subsequent two lines split the standard callby-value function application into multiple steps. The
bind v1 v2 expression creates a thunk κ by binding a
function value λ with an argument value v. A thunk may
be forced by direct invocation or indirect event dispatch.
Before a thunk may be forced, the allow v expression
allocates a handle h for a given thunk κ, which may
be viewed as a permission to force a particular thunk
instance or message. The permission to invoke may be
revoked by disallow v on a handle h. An invoke v1 v2 term
takes a handle-thunk pair h κ to construct a message m
where h must grant permission for forcing κ. A message
m is simply a handle-thunk pair (h, κ).
As an example, let λx be the execute method code
and let at be an address for an AsyncTask. The standard
function application (λx at ) would simply translate to

primitives
thunks
calls
events
forcing
binding
functions
packages

variables x ∈ Var
addresses a ∈ Addr
handles h ∈ Handle
thunks κ ∈ Thunk ::= λ[v]
messages m ∈ Msg ::= (h, κ)
stores
message stores
continuations
states

ρ ::= · | ρ[a 7→ v]
µ, ν ::= · | µ[(h, κ)]
k ::= • | let x = k in e | m | mk
σ ∈ State ::= he, ρ, µ, ν, ki | initial

Figure 4. The syntax and the semantic domains of
λlife , a core model of event-driven programs capturing
enabledness of events and allowedness of invocations.
abstracted sub-trace for object t1 from the recorded
trace in Figure 2b is as follows:

let k = bind

The reason to split function application into these steps
is that thunks and handles are now first-class values and
can be used in event dispatch.
The direct invocation expressions are mirrored with
expressions for event dispatch. An enable v expression
allocates a handle h for a given thunk κ and enables it
for the external event-processing system (i.e., gives the
event-processing system permission to force the message
(h, κ)), while the disable v expression disables the message named by a handle h. There is no expression directly
parallel to invoke v1 v2 . Instead, when an expression reduces to a value, control returns to the event-processing
loop to (non-deterministically) select another enabled
event. The force m expression is simply an intermediate
in evaluation that represents a message that is forceable
(i.e., has been permitted for forcing via allow or enable).
The remainder of the syntax is mostly standard, except that functions λ : fung x in e are tagged with a package g, which we discuss subsequently in subsection 3.3 regarding our instrumented semantics for recording traces.
The let expression is variable binding with the usual
semantics. Values v of this expression language are variables x, a variable used to bind the active event handle
me, whatever base values of interest · · · , closures λ, store
addresses a (which are the values of heap-allocated objects), thunks κ, handles h, and unit (). Messages m
do not need to be first class, as they are referred to
programmatically via their handles.

AsyncTask.<init>()
AsyncTask.execute()
PostExecuteAsyncTask.onPostExecute()

Once we have sets of sliced traces, we apply and
evaluate specification mining techniques to learn lifestate
rules. As alluded to above, the primary challenge for
mining lifestate specifications is that lifestate rules center
around event enabling-disabling and callin allowingdisallowing, which are not observable in recorded traces.
We present our mining approach in section 6 and we
evaluate them in section 7.

3.

Modeling Event-Driven Programs

In this section, we formalize a small-step operational
semantics for event-driven programs using an abstract
machine model (λlife ) that unifies enabledness for event
lifecycles and allowedness for callin typestates. Crucially,
this semantics motivates lifestate specifications, as the
concrete states of this semantics serves as the concrete
domain from which lifestate specifications abstract (section 4). This semantics also serves as a basis for describing our dynamic analysis for recording traces of events,
callbacks, and callins (section 5).
3.1

λx at in let h = allow k in invoke h k

Thunks, Handles, and Messages

The syntax of λlife is shown at the top of Figure 4, which
is a λ-calculus in a let-normal form. The first line of
expressions e are standard, including variables and values
v, control flow, and whatever base values and operations
of interest (e.g., integers, tuples) but excluding function

3.2

Semantics: Enabling Is Not Enqueuing

In contrast to the Android implementation, the state of a
λlife program does not have a queue. Rather, the external
5

Bind

Disable

Disallow

hbind λ v, ρ, µ, ν, ki −→ hλ[v], ρ, µ, ν, ki hdisable h, ρ, µ[(h, κ)], ν, ki −→ h(), ρ, µ, ν, ki hdisallow h, ρ, µ, ν[(h, κ)], ki −→ h(), ρ, µ, ν, ki

Enable

h∈
/ dom(µ)

Allow

Invoke

h∈
/ dom(ν)

(h, κ) ∈ ν

henable κ, ρ, µ, ν, ki −→ hh, ρ, µ[(h, κ)], ν, ki hallow κ, ρ, µ, ν, ki −→ hh, ρ, µ, ν[(h, κ)], ki hinvoke h κ, ρ, µ, ν, ki −→ hforce (h, κ), ρ, µ, ν, ki

Force

(h, (fung0 x0 in e0 )[v 0 ]) = m

InvokeDisallowed
m = (h, κ)

m∈
/ν

Event

(h, κ) ∈ µ

hforce m, ρ, µ, ν, ki −→ he0 [v 0 /x0 ][h/me], ρ, µ, ν, mki hinvoke h κ, ρ, µ, ν, ki −→ h(), ρ, µ, ν, •i hv, ρ, µ, ν, •i −→ hforce (h, κ), ρ, µ, ν, (h, κ)i

Figure 5. Semantics. Create thunks and allocate handles to disable, disallow, enable, and allow messages.
environment (e.g., user interactions) is modeled by the
non-deterministic selection of an enabled event. When
an event is processed, it begins execution in the current
state, so the effects of external events can be modeled
by effects on the global heap. This model eliminates the
complexity of a queue that is an implementation detail
for the purposes of lifestate specification.
We consider an abstract machine model with a store
and a continuation, and we enrich it with an enabled
events store µ, which is a finite map from handles to
thunks, and an allowed calls store ν, which is also a
map from handles to thunks. These stores can also
be seen as the set of enabled and allowed messages,
respectively. And thus a machine state σ : he, ρ, µ, ν, ki
consists of an expression e, a store ρ, enabled events
µ, allowed calls ν, and a continuation k (shown at
the bottom of Figure 4). The store ρ is a standard,
finite map from addresses a to values v. We explain the
special state initial while discussing the trace semantics
in subsection 3.3. A continuation k can be the top-level
continuation • or a continuation for returning to the
body of a let expression let x = k in e, which are standard.
Continuations are also used to record the active messages
via m and mk corresponding to the run-time stack of
activation records.
We define an operational semantics in terms of the
judgement form σ −→ σ 0 for a small-step transition relation. In Figure 5, we show the inference rules defining the
reduction steps related to creating, enabling-disabling,
allowing-disallowing, and finally forcing messages. The
Bind, Disable, Disallow, Enable, and Allow rules follow closely the informal semantics discussed previously
in subsection 3.1. Observe that Enable and Allow are
parallel in that they both allocate a fresh handle h, and
Disable and Disallow look up a message via its handle.
The only difference between Enable and Disable versus
Allow and Disallow is that the former pair manipulate
the enabled events µ, while the latter touches the allowed
calls ν. We write µ[(h, κ)] for the map that extends µ
with a mapping (h, κ) (i.e., is the same as µ except at
h) and similarly for other maps.

The Invoke and Event rules have similar parallels.
The Event rule says that when the expression is a value
v and the continuation is the top-level continuation •,
then a message is a non-deterministically chosen from the
enabled events µ to force. For instrumentation purposes
(see subsection 3.3), we overload continuations to record
the event message (h, κ) in the continuation. The Invoke
rule checks that the given handle-thunk pair is an allowed
message in ν before forcing.
The Force rule implements the “actual application”
that reduces to the function body e0 with the argument v 0
substituted for the formal x0 . So that the forced message
has ready access to its handle h, the h is substituted
for the me parameter. Observe that an enabled event
remains enabled after an Event reduction. A “dequeuing” event-processing semantics can be implemented by
an event disabling itself (via disable me) on execution.
To adequately model Android, it is important to be
able to model both events that are self-disabling (e.g.,
the event that invokes onCreate) and those that do
not self-disable (e.g., the event that invokes onClick).
Again for instrumentation purposes, we push the invocation message m on the continuation (via mk). The
InvokeDisallowed rule states that a disallowed message
invocation terminates the running program by dropping
the continuation. The Return and Finish rules simply
state that the recorded message m frames are popped
on return from a Force and Event, respectively. We
elide these rules and the remaining reduction rules, as
they are as expected.
3.3

Defining Callbacks and Observable Traces

We wish to record traces of “interesting” transitions from
which we mine lifestate specifications. Lifestate specifications abstract Enable, Disable, Allow, and Disallow
transitions, which are unfortunately unobservable or hidden. That is, they are transitions in λlife that are not
observable in an implementation like Android. Our challenge is to infer lifestate specifications from observable
transitions like, “An event message m was initiated.”
0
In Figure 6, we define the judgment form σ −→
τ σ ,
which instruments our small-step transition relation
6

transitions
observable kinds

initial state and a “dummy” init transition with an Init
rule. Any remaining rules defining the original transition
relation σ −→ σ 0 not discussed here are simply labeled
with the “don’t care” transition label ε.
We write JeK for the path semantics of λlife expressions
e that collects the finite (but unbounded) sequences of
alternating state-transition-state στ σ 0 triples according
0
to the instrumented transition relation σ −→
τ σ . From
paths, we derive traces $ in an expected manner by
keeping transitions but dropping intermediate states.
The design of the trace recording in DroidLife follows
0
this instrumented semantics σ −→
τ σ to obtain traces like
the one shown in Figure 2b. In particular, it maintains
a message stack corresponding to the continuation k to
emit callback cb and callin ci transitions.

τ ∈ T ⊆ Trans ::= oknd m | ε | init
oknd ::= evt | dis | cb | ci | ret

traces

$ ∈ Trans∗ ::= · | τ $

ForceCallback

(h, (funapp x0 in e0 )[v 0 ]) = m
fwk = pkg(k)
0 0
0
−→
hforce m, ρ, µ, ν, ki cb
m he [v /x ][h/me], ρ, µ, ν, mki

ForceCallin

(h, (funfwk x0 in e0 )[v 0 ]) = m
app = pkg(k)
0 0
0
−→
hforce m, ρ, µ, ν, ki ci
m he [v /x ][h/me], ρ, µ, ν, mki
def

msg(let x = k in e) = msg(k)
def
def
msg(m) = msg(mk) = m
def
pkg(k) = g if (h, (fung x in e)[v]) = msg(k)

Figure 6. Callbacks and callins are transitions between
framework and app code.

4.

Lifestate Specification: Abstracting
Enabledness and Allowedness

In this section, we define formally the meaning of lifestate
rules building on the λlife concrete model of event-driven
programs from section 3.
We consider the abstraction of messages to be a parameter of our approach. We call the message abstraction
ˆ and assume
of interest a message signature m
b ∈ Msg
it comes equipped with a standard concretization funcˆ → ℘(Msg) to give signatures meaning and
tion γ : Msg
ˆ
an element-wise abstraction function β : Msg → Msg
to lift a message to its signature satisfying the soundness and best-abstraction relationship. In the case of
an Android method call like (t: AsyncTask).execute()
(which corresponds to a message m : (ht , λx [at ]) for some
handle ht , function λx , and object address at ), the
message signature can be the Java method signature
AsyncTask.execute(). In DroidLife, we make a further
refinement on Java method signatures to split on values of primitive type, so Button.setEnabled(false) and
Button.setEnabled(true) are considered distinct message signatures. For the implementation, the elementwise abstraction function β is applied to recorded messages to produce message signatures for lifestate mining.
A lifestate specification R
b is a set of rules where
a rule b
r is an enable → evt, disable 9 evt, allow → ci,
or disallow 9 ci constraint. We define the meaning of
lifestate specifications by defining an abstraction of the
concrete transition relation σ −→ σ 0 for λlife .
To do so, we consider signature transitions b
τ and
a signature traces $.
b A signature transition b
τ are
simply analogous to concrete transitions τ , except over
signatures m
b instead of concrete messages m. As input
to specification mining, we are only concerned with the
event evt, callin ci, and disallowed dis transition kinds, so
we drop the callback cb and return ret kinds. A signature
trace $
b is simply a sequence of signature transitions. To
define the meaning of signature transitions and traces, we

from the previous subsection with transition labels τ .
Interesting observable transitions correspond primarily
to introduction and elimination operations on messages.
We instrument the Event rule to record that event
message m was initiated (via observable evt m). Similarly,
we instrument the InvokeDisallowed rule to record that
an invocation of a message was disallowed (via dis (h, κ)).
We use ε to instrument an uninteresting, “don’t care”
transition or an unobservable, “don’t know” transition.
The allowed invocation of a message with the Invoke
rule is an uninteresting transition, so it is simply labeled
with ε. These cases are simply adding a transition label
to the rules from Figure 5, so they are not shown here.
Recall from section 2 that we define a callback as an
invocation that transitions from framework to app code
and a callin as an invocation from app to framework
code. In λlife , this definition is captured crisply by the
context in which a message is forced. In particular,
we say that a message is a callback if the underlying
callee function is an app function (package app) and it
is called from a framework function (package fwk) as
shown in ForceCallback. The msg(·) function inspects
the continuation for the running, caller message. The
pkg(·) function gets the package of the running message.
Analogously, a message is a callin if the callee function
is in the fwk package, and the caller message is in the app
package (rule ForceCallin). There is a remaining rule
not shown here, force (ForceInternal), where there is
no switch in packages (i.e., g 0 = pkg(k) where g 0 is the
package of the callee message). It is not an interesting
transition, so it is labeled with ε.
These three cases for force replace the Force rule
from Figure 5. We also instrument the Return rule
to record returning via ret m to retain a call tree
structure in the sequence of transitions. Finally, to
simplify subsequent definitions, we introduce a “dummy”
7

νb according to the lifestate rules R.
b For example, the
Enabled rule checks if the current transition evt m
b can
happen by checking if m
b is in the enabled set µ
b. If so,
it updates the permitted state according to the rules R.
b
The helper function →evt (bı) gathers the set of messages
that is enabled by bı and similarly for disable, allow, and
disallow rules. For presentation cleanliness, we leave the
rules R
b implicit in the inference rules since it is constant.
Finally, the meaning of a lifestate specification JRK
b is
the set of signature traces that do not get stuck during
reduction (where −→∗ is the reflexive-transitive closure
R
b
of the single step relation). And this definition gives rise
to a natural description for when a trace is described by
or sound with respect to a specification:

R
b ∈ LifeSpec ::= · | R
b , br

lifestate specs
rules
br ::= bı 99K m
b
forcings bı ::= m
b | init

99K::= → evt | 9 evt | → ci | 9 ci
ˆ ::= oknd
b
τ ∈ Trans
[m
b | init

signature transitions

oknd
[ ::= evt | ci | dis

signature traces

∗

ˆ
$
b ∈Π
b ⊆ Trans
::= · | b
τ$
b
µ
b, b
ν ::= · | µ
b, m
b
ˆ ::= h$,
σ
b ∈ State
b µ
b, b
νi

signature stores
signature states
Enabled
m
b ∈b
µ

µb0 = b
µ ∪→evt (m
b)

νb0 = b
ν ∪→ci (m
b)

µb0 = b
µ ∪→evt (m
b)

νb0 = b
ν ∪→ci (m
b)

0

h(evt m
b )$
b,b
µ, b
ν i −→ h$
b , µb −9evt (m
b ), νb0 −9ci (m
b )i

Allowed
m
b ∈b
ν

0

b
Definition 1 (Trace Soundness). A signature trace $
is sound with respect to a lifestate specification R
b iff $
b
is described by R
b (i.e., $
b ∈ JRK).
b Or in other words, the
signature trace $
b can be reduced without getting stuck
(i.e., h$,
b ·, ·i −→∗ h·, µ
b, νbi for some µ
b, νb).
R
b
A specification is then sound with respect to a
λlife program if its signature traces abstract the set
of concrete traces of the program:

0

h(ci m
b )$
b,b
µ, b
ν i −→ h$
b , µb −9evt (m
b ), νb −9ci (m
b )i

Disallowed

Initialized

h(dis m
b )$
b,b
µ, b
ν i −→ h$
b,b
µ, b
νi

b
µ = →evt (init)
b
ν = →ci (init)
h(init)$
b , ·, ·i −→ h$
b,b
µ, b
νi

m
b ∈/ b
ν

def
b ∈R
b
b
m
b bı→ evt m
def
ı) = m
b bı→ ci m
b ∈R
b
→ci (b

→evt (ı) =

J·K

JR
bK

:
def

=

def
b ∈R
b
b
m
b bı9 evt m
def
ı) = m
b bı9 ci m
b ∈R
b
9ci (b

9evt (ı) =

Definition 2 (Specification Soundness). A lifestate
specification R
b is sound with respect to an expression e
iff for every trace $ of e, it is in the concretization of a
signature trace $
b of R
b (i.e., formally, JeK ⊆ γ(JRK)).
b

∗

LifeSpec → ℘(Trans )
n
o
$
b h$
b , ·, ·i −→∗ h·, b
µ, b
ν i for some b
µ, b
ν
R
b
ˆ

5.

Figure 7. Meaning of lifestate specifications. A lifestate
rule b
r is an abstraction of enabling enable v, disabling
disable v, allowing allow v, or disallowing disallow v
transitions.

Trace Slicing for Multi-Object
Event-Driven Protocols

As the specification mining problem is severely underconstrained, we wish to constrain the search space of
specifications as much as possible before applying the
learning algorithms. As a first step, we wish to slice a
trace into sub-traces that group together related messages or method invocations that (likely) correspond to
different protocols. A well-known issue is that related
method invocations may involve multiple objects. This issue is exacerbated in event-driven protocols where event
messages correspond to some internal data structures
of the framework rather than method calls per se. For
instance, in our running example, a call to the callin
(b:Button).setEnabled(. . .) that enables or disables a
button b should be associated with a Click event for b.
One reasonable and common assumption is that two
related messages should use some common values that
are readily accessible, such as arguments for method
invocations. We call this heuristic, the argument-sharing
strategy, and leave as a parameter of the strategy
a function args : Msg → ℘fin (Val) that specifies the
arguments of a message. This heuristic is similar to
the one employed by Pradel and Gross [31] for mining
multi-object API protocols. Following the argumentsharing strategy, we can slice observations so that they

lift the concretization on message signatures to signature
transitions b
τ and traces $
b in the expected way.
We can then define a signature store µ
b, νb as a set of
message signatures, which is an abstract analogue of
a message store. In a signature state σ
b : h$,
b µ
b, νbi, the
signature store µ
b is a set of enabled message signatures
(i.e., abstract messages) and νb is a set of allowed
message signatures. For convenience, we refer to the
union µ
b ∪ νb of enabled and allowed message signatures
in a state as the set of permitted signatures and all other
message signatures that are disabled or disallowed as
the prohibited signatures.
A signature state σ
b : h$,
b µ
b, νbi also includes a signature
trace $
b that controls the execution of a corresponding
abstract machine defined by the transition relation
σ
b −→R
b0 that is parametrized by a set of rules R
b and
bσ
defined in Figure 7. This transition relation is relatively
straightforward: it considers the signature transition b
τ
at the beginning of the $
b and determines whether b
τ is
permitted according to the set of permitted signatures.
If it is permitted, it updates the signature stores µ
b and
8

contain only observable transitions that share a common
argument (this strategy is essentially described as trace
slicing [14]).
However, one issue in trace slicing for event-driven
object protocols is that the messages of interest are the
event messages (in evt m) and the callin messages (in
ci m0 ). As noted above, the “argument” of interest for
the Click event message is the button b buried inside
internal implementation-specific data structures.
From the (b:Button).setEnabled(. . .) callin and
Click event example, we also see that regardless of how
b may be stored in the Click event message, the Click
event eventually invokes the callback l.onClick(b) on
some listener l where button b becomes an argument
(retrieving b in some implementation-specific manner).
Thus we extend the argument-sharing strategy to event
messages by defining the arguments of an event message
m as the arguments of any callbacks that it invokes
(instead of m’s own arguments). Once the traces have
been sliced for each object, we apply the message abstraction function β and partition the traces based on
the abstraction of the sliced object.
While our particular argument-sharing strategy focuses on associating callbacks with their initiating events,
this strategy is quite flexible in that other appropriate
context information (e.g., values reached through the
heap) could be incorporated into the trace slice.

6.

accuracy in modeling complex, often partially observable
processes. The challenge of learning a probabilistic model
of the interaction between the Android framework and
an app over the alphabet of signature messages is that
in general neither model has a direct interpretation.
For a state xi of an a HMM or PFSA A, we define the
set of permitted message signatures to be the labels of
all enabled outgoing transitions and the set of prohibited
message signatures as its complement.
For a state xi and an enabled outgoing transition
labeled m,
b we learn the lifestate enable (or resp. allow)
rules that m
b permits all message signatures prohibited
in xi but permitted in the target set of this transition.
Similarly, for the state xi and an enabled outgoing
transition labeled m,
b we learn disable (or disallow)
rules that m
b prohibits all messages permitted in xi
that become prohibited along the transition.
The final lifestate specification R
b is the union of
permit and prohibit rules of all states of the automaton.
To identify high probability rules, we associate with
each rule m
b i 99K m
bj ∈ R
b a weight that is the sum
the probabilities of all transition that define the rule
normalized by the number of permitted sets m
b i is in.
Symbolic Sampling via ]SAT. In contrast to the
two-phase probabilistic automata approaches, we propose an algorithm that directly learns a lifestate specification from the set of signature traces Π
b that is potentially
easier to interpret.
The learning algorithm proceeds by computing a
weight for each possible rule in RuleSet using the
traces in Π
b and then obtains a lifestate specification by
selecting the rules that meet a weight threshold. The
weight assigned to a rule is an average, among all the
traces in Π,
b of the fraction of the total executions that
are sound for that rule.
Intuitively, the ideal settings to compute the weight
is to observe the sequence of signature states and
transitions (a signature path). The main difficulty we
face is that the internal state of the permitted messages
(i.e., the signature state h$,
b µ
b, νbi) is not observable. To
address the problem, we propose an abstraction of the
signature paths, which we use in our learning algorithm.
We assume no prior knowledge on the internal behavior of the framework and define the most conservative
abstraction via the non-deterministic transition relation
σ
b −→n σ
b0 that, upon invoking a permitted enable or allow
signature transition b
τ , can non-deterministically change
the internal state of the system (i.e., permits or prohibits
any other message) but keeps the semantics of disallow
and disables as in Figure 7. This choice of abstraction
may produce a large number of spurious behaviors that
could affect the quality of rules we learn, but we make
the following observations: (i) the imprecision introduced
by the spurious transition may be reduced by observing

Mining Lifestate Specifications

In the previous sections, we formalized a model for eventdriven systems like Android centered around enabled
events and allowed callins. From this model, we derive
the notion of lifestate specifications. In this section, we
discuss an application of specification mining techniques
to learn lifestate specifications. For a set of signature
traces Π,
b let Σ be the set containing all the abstract
messages contained in the traces Π
b and init. We learn
specifications where the messages in the rules are elements of Σ, hence restricting our learning algorithms to
an abstraction of messages that we observed concretely.
We denote with RuleSet the set of all the possible rules
that can be learned from Σ.
The goal of the mining algorithms is to find a specification R
b ∈ ℘(RuleSet) and to this end we consider 3
different approaches. Two of these are applications of an
off-the-shelf machine learning tool Treba [23] learning
probabilistic models of the interaction between the app
and the Android framework, and a symbolic sampling
one based on model counting of propositional Boolean
formulas [20], implemented with pySMT [19] and the
solver sharpSAT [35].
Probabilistic Models. Hidden Markov Models (HMM) and Probabilistic Finite State Automata (PFSA) are
common statistical models famed for their simplicity and
9

a large number of traces; (ii) with a further knowledge
of the framework, we can reduce the non-determinism
(i.e. reducing the abstract paths), hence improving the
quality of the learned specification.
The main challenge with this approach is that enumerating all abstract paths for a signature trace is intractable. To overcome this problem, we represent the
set of possible abstract paths symbolically encoded as a
propositional logic formula, to leverage efficient model
counting solvers.

Research Questions. Given a candidate specification (i.e., a set of lifestate rules) obtained from a learning
method, we consider the following research questions.

Learn Specifications by Counting Paths. Given a signature trace $
b:b
τ1 ...b
τ n , let Paths($)
b denotes the set
of all the sequences of states and transitions (paths) under the non-deterministic semantics. For each rule kind
bı→ evt m
b (resp. 9 evt, → ci, 9 ci), we say that the rule is
“matched” in a state of the path if, in that state, the message m
b is enabled (resp. disabled, allowed, disallowed)
and the abstract transition executes the message bı.
We want to count all the paths of a trace such that
the ratio of the number of states of the path that match
the rule over the total number of times we seen bı in the
trace is greater than a weight w. For a signature trace
$,
b we call RulePaths($,b
b r) such set of paths.
Given a signature trace $
b and a rule b
r, the frequency
of b
r in $
b with weight w, is given by:

• RQ2 (Veracity): For each rule in a mined specifi-

def

Freq(w,b
r, $)
b =

• RQ1 (Sufficiency): Is a mined specification sound with

respect to previously unseen traces? We say that a
specification is sufficient for explaining a set of traces
if each trace is sound with respect to the specification
(according to Definition 1 in section 4). Foremost, we
seek specifications that are, in the limit, sufficient to
explain all actual Android behavior.
cation, does the rule correspond to actual Android
behavior? We say that a specification is veracious
if it captures when a message should be enabled or
allowed during the execution of an app and when it
should not. In the end, we want to find rules that in
fact describe the true enabling, disabling, allowing,
and disallowing behavior of Android.
Experimental Methodology. We consider the mining algorithms from section 6 based on probabilistic models (HMM and PFSA) and symbolic sampling (]SAT).
For the symbolic sampling approach, we use two weight
thresholds 0.6 and 0.8, corresponding intuitively to keeping only the rules that explain slightly more than half
the paths and those that explain most paths, respectively. This selection of parameters gives us four learning
methods to evaluate that we abbreviate as ]SAT-0.6,
]SAT-0.8, HMM, and PFSA.
Traces recorded by DroidLife are sliced for each object,
abstracted into message signatures, and grouped by the
framework type of the slicing object. Thus, we have a
corpus of sliced and abstracted traces for each framework
type of interest. To evaluate a learning method, we divide
a trace corpus into a training set and a testing set using
5-fold cross validation.

|RulePaths($,b
b r)|
.
|Paths($)|
b

The notion can naturally be lifted to a set of signature
traces Π
b by taking the geometric mean of the fractions
of the observed traces.
Let δ be a real constant. The final specification is
def
R
b = {b
r | Freq(w,b
r, Π)
b ≥ δ}. The threshold δ is needed
to select only the rules that, according to the frequency
value, more likely capture the framework behavior.
The number of paths in the sets Paths($)
b and
RulePaths($,b
b r) is exponential in the total number
of messages. Thus, it is not feasible to explicitly enumerate them. Our solution is to encode all the paths in
Paths($)
b as a propositional logic formula. The intuition
is that each (complete) model of this formula represents
a path in Paths($).
b Hence, we cast the problem of
counting the cardinality of Paths($)
b to the problem of
counting the number of models of the Boolean formula,
for which several efficient tools exist (e.g. [35]). The encoding is an adaptation of Bounded Model Checking [10],
a technique that encodes all the paths of length k of a
transition system.

7.

Corpus: Generating Sliced and Abstracted Traces
We begin with 133 traces of running Android applications recorded by DroidLife. These traces were generated
from a corpus of 1909 apps retrieved from Github.
We used two different methods for generating traces:
manual exercising of the app and automatic by means
of the UI Exerciser Monkey. We chose to generate some
traces using manual exercising because apps require user
logins, API keys, and other inputs that present problems
for automatic exploration tools (e.g., [5, 8, 27]). The
manual method resulted in 65 traces and the automatic
in 68. The process for manual trace generation was to
exercise the app in a normal manner for 10 minutes under
instrumentation. For the automatic Monkey, a script
loaded the application on an Android emulator, waited
3 minutes for any application initialization, and then
pulsed the UI exercising 40 times. Each time inputting
50 random events and delaying 30 seconds in between.

Empirical Evaluation: Mining

Here, we evaluate empirically whether our process finds
meaningful lifestate specifications, as well as compare
the quality of the specifications obtained from different
mining algorithms.
10

Table 1. The data set is partitioned by framework type
(f-type) on the sliced object. For each trace set, we
give the number of traces, the average length of the
traces (len), the total number of distinct event message
signatures (evts), callin signatures (cis), and the size of
the specification space (|LifeSpec|).

Table 2. Mined candidate specifications. For each trace
set for a framework type, we apply each method to learn
on a training set (using 5-fold cross validation). This
table shows the number of lifestate rules of each kind
on the first training set.
lifestate rules

traces

len

evts

cis

|LifeSpec|

(num)

(mean)

(num)

(num)

(num)

Fragment
FragmentV4
Button
AsyncTask

52
124
654
63

9.7
9.0
4.6
3.8

6
10
4
1

19
34
28
4

1275
3916
2080
55

summary

893

6.8

21

85

7326

f-type

→ evt

From the corpus of 133 recorded traces, we apply
callback-driven trace slicing from section 5 to get 6134
sliced traces over 184 framework types. Each framework
type corresponds to a partition of the 6134 sliced traces.
We selected four of these framework types, which had
trace sets of sufficient length and diversity of events
and callins, for evaluating our learning methods. In
Table 1, we list some statistics about the data set.
The specification space (|LifeSpec|) is the number of
possible lifestate rules as determined by the number of
observed events (evts) and callins (cis). The summary
line is the total number of traces, the mean of mean
length of traces, the total number of event and callin
signatures, the total specification space.

f-type

method

Fragment
Fragment
Fragment
Fragment
FragmentV4
FragmentV4
FragmentV4
FragmentV4
Button
Button
Button
Button
AsyncTask
AsyncTask
AsyncTask
AsyncTask

]SAT-0.6
]SAT-0.8
HMM
PFSA
]SAT-0.6
]SAT-0.8
HMM
PFSA
]SAT-0.6
]SAT-0.8
HMM
PFSA
]SAT-0.6
]SAT-0.8
HMM
PFSA

total

(num)

9 evt
(num)

→ ci
(num)

9 ci
(num)

2
0
7
12
2
0
39
27
7
2
29
20
1
0
2
1

0
0
12
14
0
0
24
45
1
1
22
25
0
0
4
2

17
3
48
39
24
2
235
145
30
7
87
87
2
1
6
5

5
0
32
41
2
0
209
213
7
4
89
90
0
0
8
5

151

150

738

705

Sound Traces (frac/on)

Suﬃciency

Candidate Specifications. In Table 2, we show the
number of each rule kind learned using each method
on the first training set. Our first observation is that
the probabilistic model-based methods generate many
more candidate rules than the symbolic sampling-based
method. This observation is not unexpected, as the symbolic sampling-based method takes a more conservative
approach for generating rules: it generates rules based
on the frequency of explainable signature traces. Our
second observation is that event-disables are the least
frequently derived rules. This observation is also not
unexpected, as event-disables are the least constrained
rule kind. The total line is the total number of rules
of each kind. The magnitude is not meaningful, but it
shows the relative frequency of the rule kinds.

1
0.8
0.6
0.4
0.2
0

Fragment
Fragment v4
Bu;on
AsyncTask
Average

SAT-0.6

SAT-0.8

PFSA

HMM

Learning Method

Figure 8. Sufficiency measures the fraction of sound
traces of a given testing set for a given specification
(higher is better). For each training set for a framework
type, we measure sufficiency for each learned specification on the corresponding testing set. The y-axis shows
the average sufficiency measure over the testing sets
(from 5-fold cross validation) for each framework type
grouped by learning method. The rightmost bar in each
group shows the average over the four framework types.

RQ1: Measuring Sufficiency. Given a testing set
and a candidate specification, we measure sufficiency as
the ratio of traces that are sound with respect to the
specification to the number of traces in the testing set.
Figure 8 shows the sufficiency measure for each
learned specification, grouped by method. No one
method dominates the others by this measure. For
example, the PFSA method is the only one that gen-

erates rules that have soundness fraction over 0.5 for
Fragment but is worse than all other methods for AsyncTask.
The sufficiency measure for ]SAT-0.8 is generally high,
but recall from Table 2 that ]SAT-0.8 learns far fewer
rules than the other methods. It is quite conservative in
the rules it learns, but for the rules that it does learn,
11

each column. Since no single method dominated most
of the time, this row shows that the combination of
methods can learn a more complete specification than
any single method alone. In total we learned 75 unique
rules which model the behavior of the framework. Of
these, 55 directly correspond to the cause and effect that
a developer would attribute to the system.
The highest level point is that a number of actual
rules are learned for each framework type by both learning methods (the actual column) out of the thousands of
possible rules shown in Table 1 (7326) by only examining
the top 20 rated rules from each learning method. And
furthermore, most actual rules that are learned correspond to the real root cause in the Android framework
(the direct column). This observation provides supporting evidence for lifestate rules capturing event-driven
object protocols at an appropriate level of abstraction.
The only exception to the high fraction of actual rules
is the AsyncTask which can be fully specified by 7 rules as
we describe further below. This biases the fraction to be
low since we took the top 20 rated rules, and there were
only 7 rules to learn. And every specification needed for
AsyncTask was learned. Furthermore, most of the direct
rules are found even in the top 10.
One remaining question is how many rules are required to specify the protocol. Is it the case that the
number of rules for each framework type should be small
compared to the number of possible rules. To address
this question, we manually specified the full set of rules
for AsyncTask for the observed events and callins (since
this class is comparatively small with only 55 possible
rules compared to the thousands possible for the other
framework types, see Table 1).
Manual specification of AsyncTask resulted in 7 direct
rules. The result is that we are learning 3 out of the
7 direct rules with the ]SAT-0.6 method, 4 out of 7
with the PFSA method, and 6 out of 7 with the HMM
method. There were no rules in the manually created
set which were not learned by one of our algorithms.

Table 3. Veracity is a measure of precision in finding
actual rules by manually triaging the rules found by each
learning method. The actual column shows the number
of learned rules that correspond understood Android
behavior. The direct shows the number of actual rules
that also correspond to the root enable, disable, allow,
or disallow in Android.
rules

actual

direct

num

num

num (frac)

Fragment
Fragment
Fragment
Fragment

method
]SAT-0.6
PFSA
HMM
total unique

20
20
20
42

10
14
5
22

7
11
4
18

(0.7)
(0.8)
(0.8)
(0.8)

FragmentV4
FragmentV4
FragmentV4
FragmentV4

]SAT-0.6
PFSA
HMM
total unique

20
20
19
58

8
12
11
24

7
10
9
19

(0.9)
(0.8)
(0.8)
(0.8)

Button
Button
Button
Button

]SAT-0.6
PFSA
HMM
total unique

20
20
20
49

6
7
3
14

3
7
3
11

(0.5)
(1 )
(1 )
(0.8)

AsyncTask
AsyncTask
AsyncTask
AsyncTask

]SAT-0.6
PFSA
HMM
total unique

3
13
19
22

3
10
12
15

3
4
6
7

(1 )
(0.4)
(0.5)
(0.5)

all objects

total unique

171

75

f-type

55 (0.7)

they tend to generalize well. The ]SAT-0.6 and PFSA
methods appear to balance producing more candidate
rules and ones that generalize reasonably well. We thus
consider manual triage of the rules produced by these
two methods for evaluating veracity.
RQ2: Evaluating Veracity. To evaluate veracity,
we take a candidate lifestate specification and manually
triage the rules and categorize them with respect to
the correctness in capturing the true behavior of the
Android framework. We consider the following categories
of correctness: (actual) the rule abstracts understood
Android behavior from reading Android documentation
or the framework code; (direct) the rule is actual and
corresponds to the root cause in Android (e.g., a learned
enable rule corresponds to direct enabling in Android);
(false or unknown) the rule appears to contradict
understood Android rules. If we cannot be sure that
a learned rule corresponds to a actual rule, then we
conservatively classify it as false.
In Table 3, we show veracity results for the ]SAT-0.6,
PFSA, and HMM methods for each framework type. We
manually triaged the twenty rules with highest weight
(using the parsimony assumption that the number of
rules for each framework type should be small). We
then add a row for the total number of unique rules in

Threats to Validity. The rules that can be learned
are limited by the observations available in the traces.
For example, there was no opportunity to learn anything
about the AsyncTask.cancel() callin since our traces did
not include any observations of such an invocation. In
the end, we are limited by the extent by which framework
behavior can be explored through dynamic execution.
To try to mitigate this affect, we made traces with
as many applications as possible minimizing duplicate
traces. This exposes us to more possible ways developers
may use a given framework object. There is a potential
for bias in selecting the framework types on which to
mine specifications. To minimize this effect, we selected
by looking just at the number and length of traces and
diversity of events and callins (from Table 1).
12

Mined Specifications. From the veracity summary,
the ]SAT-0.6, PFSA, and HMM methods appear comparable, so we look more closely into the rules that
are learned. From our running example in section 2,
the most important rule that we would expect is that
(t:AsyncTask).execute() callin can only be called once.
It is indeed learned by all three methods. Another important rule is that the PostExecute event is enabled
by the (t:x AsyncTask).execute() callin. In this case,
the ]SAT-0.6 and HMM methods learned this rule but
the PFSA method did not.
The biggest source of false rules learned that we observed are rules that appear to come from common patterns in how developers use the framework. For example,
one rule learned by PFSA is that (b:Button).getWidth()
disallows itself, which perhaps corresponds to few traces
with repeated calls to getWidth.
A source of actual but not direct rules relates to
callbacks and super calls. We found that a common
pattern in Android is to require a call to the super
method. For example to implement onActivityCreated,
super.onActivityCreated would need to be called.
Thus in functioning applications, this super call is seen as
a callin that always happens with the event the triggers
the onActivityCreated callback. Thus, the left-hand–
side of a actual but not necessarily direct rule is where
the left-hand–side is either the event or the super callin.
One could reasonably consider removing required super
calls from our definition of callins.
In the end, we found a rule that captures an
undocumented behavior of Android in the official
Android documentation. The rule states that the
(f:Fragment).getResources() is allowed when the event
ActivityCreated that triggers the onActivityCreated
callback. The getResources callin will throw an exception if called before this ActivityCreated event.

8.

for lifecycle events in addition to their interaction with
typestate APIs for frameworks.
Other work also simplifies automata specifications
by considering simpler rule-based approaches (e.g., [18,
38]). Subsequently, Lo et al. [25] extend this kind
of specification to QBEC (quantified binary temporal
rules with equality constraints) specifications. However,
these rule-based approaches differ from lifestate rules
in that they express necessary causation (e.g for every
lock there must be a subsequent unlock). In contrast,
lifestate rules do not express such conditions, and these
conditions are actually undesirable, as most events in
event-driven systems enable other events but do not
cause them to occur.
Concerning static mining techniques, Alur et al. [4]
propose a technique to infer a typestate interface for
a given Java class. This technique could conceivably
be used to statically infer typestate specifications for
event-driven frameworks such as Android. However, their
technique does not account for the unique relationship
between typestate and lifecycle events in event-based
systems. Additionally, Shoham et al. [34] develop a technique for inferring the typestate of a certain API by analyzing presumably correct client programs. The order of
method invocations, determined statically, can produce
a multi-object typestate specification. Ramanathan et al.
[33] propose a similar technique, but one that can also
derive invariant-based preconditions. However, to our
knowledge these techniques also cannot be successfully
extended to event-based systems, where typestate and
lifecycle properties may interact.
Analysis of Event-Driven Systems. Recently,
more and more program analyses have focused on eventdriven systems. Both dynamic analyses, such as for race
detection [22, 29], and static analyses for information
flow [7] and safety properties [11] expect some specification of framework behavior with respect to callbacks.
There has also been a number of recent static analyses
targeting information flow concerns (e.g., [16, 21, 37])
where a significant concern is synthesizing models for
taint flow through the framework [9].
There are also some tools concerned with exposing
the implicit control flow from the framework to callbacks
by linking callback registration methods with their
callbacks [13, 28], modeling GUI components [41], and
explicating reflection [12]. This information is useful for
creating an over-approximation of the possible callbacks
but does not capture precise events that may enable or
disable a given event that then invokes the callback.

Related Work

Specification Mining. Our technique is broadly similar to mining typestate specifications for API interfaces
from traces (e.g., [3, 6, 15, 17, 31, 36, 39, 40]). Our contribution can be seen as an extension that, in addition
to inferring typestate properties, also infers the ordering constraints of lifecycle events that interleave and
interact with typestate properties. Ammons et al. [6]
presents one of the earliest attempts to infer temporal
specifications of programs by mining observed traces.
Notably, Yang et al. [40] extend the technique to scale to
larger data-sets with imperfect traces, and Pradel and
Gross [31] improve the technique to mining specifications
for collaborations involving multiple, interacting objects.
There is also work on combining automata mining with
value-based invariant mining [24, 26]. However, we are
unaware of any previous work that mines specifications

9.

Conclusion

We have presented lifestate rules, a language for specifying event-driven object protocols. The key idea underlying lifestate rules is a model of event-driven programs
13

in terms of enabled events and allowed callins unified
as suspended messages. As a result, lifestate rules are
able to capture mixed lifecycle and typestate constraints
at a higher level abstraction than automata. We then
instantiated this model in a dynamic analysis tool called
DroidLife that prepares Android traces for specification
mining using a notion of trace slicing adapted to events
and callbacks. Finally, we applied specification mining
techniques to infer lifestate specifications based on unsupervised automata-based learning techniques that have
been previously applied to typestate mining, as well as a
direct lifestate mining technique based on propositional
model counting. In the end, we were able to learn several actual lifestate rules that accurately capture the
behavior of Android in a compact way.

[11] S. Blackshear, B. E. Chang, and M. Sridharan. Selective
control-flow abstraction via jumping. In Object-Oriented
Programming Systems, Languages, and Applications
(OOPSLA), 2015.
[12] S. Blackshear, A. Gendreau, and B. E. Chang. Droidel:
A general approach to Android framework modeling. In
State of the Art in Program Analysis (SOAP), 2015.
[13] Y. Cao, Y. Fratantonio, A. Bianchi, M. Egele, C. Kruegel,
G. Vigna, and Y. Chen. Edgeminer: Automatically
detecting implicit control flow transitions through the
android framework. In Network and Distributed System
Security (NDSS), 2015.
[14] F. Chen and G. Rosu. Parametric trace slicing and monitoring. In Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), 2009.
[15] V. Dallmeier, C. Lindig, A. Wasylkowski, and A. Zeller.
Mining object behavior with ADABU. In Dynamic
Systems Analysis (WODA), 2006.

References
[1] AntennaPod - FeedRemover bug report.
https:
//github.com/AntennaPod/AntennaPod/issues/1304.
Accessed: 2016-03-13.

[16] Y. Feng, S. Anand, I. Dillig, and A. Aiken. Apposcopy:
Semantics-based detection of Android malware through
static analysis. In Foundations of Software Engineering
(FSE), 2014.

[2] Facebook
SDK
for
Android
AsyncTask
bug report.
https://github.com/facebook/
facebook-android-sdk/pull/315. Accessed: 2016-0313.

[17] M. Gabel and Z. Su. Javert: Fully automatic mining
of general temporal properties from dynamic traces. In
Foundations of Software Engineering (FSE), 2008.

[3] M. Acharya, T. Xie, and J. Xu. Mining interface specifications for generating checkable robustness properties.
In Software Reliability Engineering (ISSRE), 2006.

[18] M. Gabel and Z. Su. Online inference and enforcement
of temporal properties. In International Conference on
Software Engineering (ICSE), 2010.

[4] R. Alur, P. Černý, P. Madhusudan, and W. Nam.
Synthesis of interface specifications for Java classes. In
Principles of Programming Languages (POPL), 2005.

[19] M. Gario and A. Micheli. pySMT: a solver-agnostic
library for fast prototyping of smt-based algorithms.
In Workshop on Satisfiability Modulo Theories (SMT),
2015.

[5] D. Amalfitano, A. R. Fasolino, P. Tramontana, S. D.
Carmine, and A. M. Memon. Using GUI ripping for
automated testing of Android applications. In Automated
Software Engineering (ASE), 2012.

[20] C. P. Gomes, A. Sabharwal, and B. Selman. Model
counting. In Handbook of Satisfiability. 2009.
[21] M. I. Gordon, D. Kim, J. Perkins, L. Gilham, N. Nguyen,
and M. Rinard. Information-flow analysis of Android
applications in DroidSafe. In Network and Distributed
System Security (NDSS), 2015.

[6] G. Ammons, R. Bodı́k, and J. R. Larus. Mining
specifications. In Principles of Programming Languages
(POPL), 2002.

[22] C.-H. Hsiao, J. Yu, S. Narayanasamy, Z. Kong, C. L.
Pereira, G. A. Pokam, P. M. Chen, and J. Flinn. Race
detection for event-driven mobile applications. In Programming Language Design and Implementation (PLDI),
2014.

[7] S. Arzt, S. Rasthofer, C. Fritz, E. Bodden, A. Bartel,
J. Klein, Y. L. Traon, D. Octeau, and P. McDaniel.
FlowDroid: Precise context, flow, field, object-sensitive
and lifecycle-aware taint analysis for Android apps.
In Programming Language Design and Implementation
(PLDI), 2014.

[23] M. Hulden. Treba: Efficient numerically stable EM for
PFA. In Grammatical Inference (ICGI), 2012.

[8] T. Azim and I. Neamtiu. Targeted and depth-first
exploration for systematic testing of Android apps. In
Object-Oriented Programming Systems, Languages, and
Applications (OOPSLA), 2013.

[24] D. Lo and S. Maoz. Scenario-based and value-based
specification mining: Better together. In Automated
Software Engineering (ASE), 2010.

[9] O. Bastani, S. Anand, and A. Aiken. Specification
inference using context-free language reachability. In
Principles of Programming Languages (POPL), 2015.

[25] D. Lo, G. Ramalingam, V.-P. Ranganath, and
K. Vaswani. Mining quantified temporal rules: Formalism, algorithms, and evaluation. Sci. Comput. Program.,
77(6), 2012.

[10] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic
model checking without bdds. In Tools and Algorithms
for the Construction and Analysis of Systems (TACAS),
1999.

[26] D. Lorenzoli, L. Mariani, and M. PezzÃĺ. Automatic generation of software behavioral models. In International
Conference on Software Engineering (ICSE), 2008.

14

[27] A. Machiry, R. Tahiliani, and M. Naik. Dynodroid: an
input generation system for Android apps. In European
Software Engineering Conference and Foundations of
Software Engineering (ESEC/FSE), 2013.
[28] M. Madsen, F. Tip, and O. Lhoták. Static analysis of
event-driven node.js javascript applications. In ObjectOriented Programming Systems, Languages, and Applications (OOPSLA), 2015.
[29] P. Maiya, A. Kanade, and R. Majumdar. Race detection
for Android applications. In Programming Language
Design and Implementation (PLDI), 2014.
[30] S. Pomeroy.
Complete Android Fragment and
Activity lifecycle.
https://github.com/xxv/
android-lifecycle. Accessed: 2016-03-13.
[31] M. Pradel and T. R. Gross. Automatic generation of
object usage specifications from large method traces. In
Automated Software Engineering (ASE), 2009.
[32] M. Pradel, C. Jaspan, J. Aldrich, and T. R. Gross.
Statically checking API protocol conformance with
mined multi-object specifications. In International
Conference on Software Engineering (ICSE), 2012.
[33] M. K. Ramanathan, A. Grama, and S. Jagannathan.
Static specification inference using predicate mining.
In Programming Language Design and Implementation
(PLDI), 2007.
[34] S. Shoham, E. Yahav, S. Fink, and M. Pistoia. Static
specification mining using automata-based abstractions.
In Software Testing and Analysis (ISSTA), 2007.
[35] M. Thurley. sharpSAT - counting models with advanced
component caching and implicit BCP. In Theory and
Applications of Satisfiability Testing (SAT), 2006.
[36] N. Walkinshaw and K. Bogdanov. Inferring finitestate models with temporal constraints. In Automated
Software Engineering (ASE), 2008.
[37] F. Wei, S. Roy, X. Ou, and Robby. Amandroid: A
precise and general inter-component data flow analysis
framework for security vetting of Android apps. In
Computer and Communications Security (CCS), 2014.
[38] W. Weimer and G. C. Necula. Mining temporal specifications for error detection. In Tools and Algorithms
for the Construction and Analysis of Systems (TACAS),
2005.
[39] J. Whaley, M. C. Martin, and M. S. Lam. Automatic
extraction of object-oriented component interfaces. In
Software Testing and Analysis (ISSTA), 2002.
[40] J. Yang, D. Evans, D. Bhardwaj, T. Bhat, and M. Das.
Perracotta: Mining temporal API rules from imperfect
traces. In International Conference on Software Engineering (ICSE), 2006.
[41] S. Yang, D. Yan, H. Wu, Y. Wang, and A. Rountev.
Static control-flow analysis of user-driven callbacks in
Android applications. In International Conference on
Software Engineering (ICSE), 2015.

15

