DroidStar: Callback Typestates for Android Classes
Arjun Radhakrishna Nicholas V. Lewchenko Shawn Meier Sergio Mover Krishna Chaitanya Sripada Damien Zufferey Bor-Yuh Evan Chang Pavol Černý





2018
2018
acmlicensed
[ICSE '18]ICSE '18: 40th International Conference on Software Engineering May 27-June 3, 2018Gothenburg, Sweden
ICSE '18: ICSE '18: 40th International Conference on Software Engineering , May 27-June 3, 2018, Gothenburg, Sweden
15.00
10.1145/3180155.3180232
978-1-4503-5638-1/18/05







This work was done while Arjun Radhakrishna was employed at the University of Pennsylvania.

  Microsoft




  University of Colorado Boulder




  University of Colorado Boulder




  University of Colorado Boulder




  University of Colorado Boulder




  Max Planck Institute for Software Systems




  University of Colorado Boulder




  University of Colorado Boulder




Event-driven programming frameworks, such as Android, are based on
components with asynchronous interfaces. The protocols for interacting with
these components can often be described by finite-state machines we
dub callback typestates.  Callback typestates are akin
to classical typestates, with the difference that their outputs
(callbacks) are produced asynchronously.  While
useful, these specifications are not commonly available, because
writing them is difficult and error-prone.


Our goal is to make the task of producing callback typestates
significantly easier. We present a callback typestate assistant tool,
, that requires only limited user interaction to produce a
callback typestate. Our approach is based on an active learning
algorithm, . We improved the scalability of equivalence queries
(a key component of ), thus making active learning tractable on
the Android system.


 We use to learn callback typestates for Android
classes both for cases where one is already provided by the
 documentation, and for cases where the documentation is unclear.
The results show that learns callback typestates
accurately and efficiently.
Moreover, in several cases, the synthesized callback
typestates uncovered surprising and undocumented behaviors.





: Callback Typestates for Android Classes
    Pavol Černý
    December 30, 2023
=========================================







§ INTRODUCTION



Event-driven programming frameworks interact with client code using
callins and callbacks.
Callins are framework methods that the client invokes and callbacks
are client methods that the framework invokes.
The client-framework interaction is often governed by a protocol that
can be described by a finite-state machine we call callback
  typestate. Callback typestates are akin to classical typestates <cit.>, with the key
 difference that their outputs (callbacks) are produced asynchronously.
Our goal is to make the task of producing callback typestates
significantly easier for developers.

As an example of a callback typestate, consider a typical interaction
between a client
application and the framework when the client wants to use a
particular service.
The client asks for the service to be started by invoking an
startService callin.
After the framework receives the callin, it asynchronously starts
initializing the service.
When the service is started and ready to be used, the framework
notifies the client by invoking a onServiceStarted
callback.
The client can then use the service.
After the client finishes using the service, it invokes a
shutdownService callin to ask the framework to stop the
service.



  
Callback typestates.
Callback typestates are useful in a number of ways, but they are
notoriously hard to produce.
First, callback typestates are a form of documentation.
They tell client application programmers in what order to invoke
callins and which callback to expect.
Android framework documentation for some classes already uses pictures very
similar to callback typestates (Figure <ref>).
Second, callback typestates are useful in verification of
client code.
They enable checking that a client uses the framework correctly.
Third, even though we infer the callback typestates from framework
code, they can be used for certain forms of framework verification.
For instance, one can infer typestates for different versions of the
framework, and check if the interface has changed.

Callback typestates are very hard to produce manually. On one hand,
inspecting code to see in what situation a callback arrives, and what
callins are enabled after that is error-prone.
Even developers familiar with the framework often miss corner-case
behaviors.
On the other hand,
obtaining the callback typestate with manual testing is hard. One
would need to run all sequences of callins, mixed in sequence with the
callbacks they produce.  We systematize this testing approach using an
active learning algorithm.



  
Callback typestate assistant .
We present a tool that makes producing callback typestates
significantly easier. Our target user is a developer who wrote an
Android class that interacts asynchronously using callbacks with
client code.
is a comprehensive framework for semi-automatically inferring
callback typestates.  The required user interaction
happens in multiple steps.
In the first step, the user provides code
snippets to perform local tasks, such as code for class initialization
and code for invoking each callin (similarly as in unit tests).
This is sufficient as long as certain widely applicable assumptions
hold. First, we assume that each sequence of callins produces a
sequence of callbacks deterministically
(this assumption fails when for instance a callback has a parameter
that is ignored at first by but that influences the typestate).
Second, we assume that the resulting typestate is finite.
If these assumptions fail, in the following steps, asks the user
for a solution to the problem.
For instance, one way to remove non-determinism is to refine one
callback into two separate logical callbacks, based on the
parameter values.
This design allows to offer the user control over the final
result while requiring only limited, local, insight from the
user.
is available for download at 




  
Approach.
We present a method for inferring typestates for Android classes.
However, our method is equally applicable in other contexts.
The core algorithm is based on Angluin's algorithm <cit.> adapted to Mealy
machines <cit.>.
In this algorithm, a learner tries to learn a finite-state machine —
in our case a
callback typestate — by asking a teacher membership and
equivalence queries.
Intuitively, a membership query asks for outputs corresponding to a
sequence of input callins, and the equivalence query asks if the learned
typestate is correct.
We note that the teacher does not need to know the solution, but only
needs to know how to answer the queries.


The key question we answer is how to implement oracles for the
membership and equivalence queries.
We show how to implement membership queries on Android classes using
black-box testing.
Our main contribution here is an efficient algorithm for implementing the
equivalence query using membership query. The insight here is that
the number of membership queries can be bounded by a function of a new
bound we call the distinguisher bound. We empirically confirmed that for
Android classes, the distinguisher bound is significantly
smaller than the state bound used in previous
work <cit.>. Given that the number of required
membership queries depends exponentially on the distinguisher bound, the novel bound is what enables our tool
to scale to Android classes.




  
Results.
We use to synthesize callback typestates for 16 Android framework
classes and classes from Android libraries.
The results show that learns callback typestates accurately and
efficiently.
This is confirmed by documentation, code inspection, and manual
comparison to simple Android applications.
The running time of on these benchmarks ranged between 43
seconds and 72 minutes, with only 3 benchmarks taking more than 10
minutes.
The usefulness of the distinguisher bound was also confirmed. Concretely, using
previously known bounds, learning the callback typestate for one of
our examples (MediaPlayer)
would take more than
a year, whereas with the distinguisher bound, this example takes around 72 minutes.
Furthermore, by inspecting our typestates, we uncovered corner cases
with surprising behavior that are undocumented and might even be
considered as bugs in some cases. For instance, for the commonly used AsyncTask
class, if execute
is called after cancel but before the onCancelled
callback is received, it will not throw an exception but will never
cause the asynchronous task to be run.
Section <ref> presents our results in more detail.




  
Contributions.
The contributions of this paper are:
[(a)]

  * We introduce the notion of callback typestates and develop an approach, based on the algorithm, to infer them.

  * We show how to implement efficiently membership and equivalence oracles required by the algorithm.

  * We evaluate our approach on examples from the Android framework, and show its accuracy and effectiveness.





§ WORKFLOW AND ILLUSTRATIVE EXAMPLE



We use the Android Framework's MediaPlayer class to explain the
standard workflow for inferring callback typestate using .
This class is highly stateful—its interface includes many methods that
are only meaningful or enabled in one or two particular player
states—and makes extensive use of callins and callbacks to handle
the delays of loading and manipulating large media files.  These
properties make callback typestate a perfect fit; in fact, MediaPlayer has one of the very few examples
where we found a complete callback typestate
specification in the Android libraries documentation.
This callback typestate is shown in Figure <ref>.





In Figure <ref>, callins are
represented by single arrows and callbacks by double arrows.
Let us look at one part of the protocol that governs the
client-framework interaction.
The client first invokes the callin setDataSource, and the
protocol transitions to the Initialized state.
In this state, the client can invoke the callin prepareAsync,
and the protocol transitions to the Preparing state.
In the Preparing state, the client cannot invoke any callins, but
the framework can invoke the onPrepared callback, and then
the protocol transitions to the Prepared state.
At this point, the client can invoke the start callin, and
the media starts playing.

Our goal is to semi-automatically infer the callback typestate from the
figure using the tool .
The developer interacts with in several steps, which we describe
now.



 §.§ Developer-Provided Snippets

To apply to the MediaPlayer class, the developer provides a
number of code snippets detailed below that act as an interface through
which the tool can examine MediaPlayer instances.



  
Test object and environment instantiation.
The main callback typestate inference algorithm of works roughly
by repeatedly performing tests in the form of sequences of method calls
on an object of the given class, i.e., the MediaPlayer.
Each test must begin with an identical, isolated, class object, and if
necessary, a standard environment.
In the first step, the developer provides a snippet to
initialize such an object and environment.
In the case of MediaPlayer, this snippet is as simple as
discarding the previous instance, creating a new one with new
MediaPlayer(), and registering the necessary callback listeners
(explained in the Callback instrumentation paragraph below).

In some cases this snippet is more complex.  As an example, we cannot
create new instances of the BluetoothAdapter class, so for that
class this snippet would need to bring the existing instance back to a
uniform initial state.




  
Callin declaration. The next step is to declare the
alphabet of “input symbols” that represent the callins in the
interface of our class—the final callback typestate will be written
using these symbols—and map each symbol to the concrete code snippet
it represents.  In most cases, there is a one-to-one correspondence
between input symbols and callin methods.  For example,
the code snippets associated with the input symbols prepare, prepareAsync, and start are prepare();, prepareAsync();, and start();, respectively.

In some cases, such as when a callin takes a parameter, the developer
may instead map a symbol to a set of code snippets representing
alternative forms of the input which are suspected to have different
behavior.  In the MediaPlayer class, the setDataSource
callin method takes a URL argument.  The developer might (rightly)
believe that depending on the validity and reachability of the given
URL, the behavior of the callin in the typestate may differ.  In this
case, the developer may provide the two snippets setDataSource(goodURL); and setDataSource(badURL); for the
same callin.  will consider both snippets for generating tests,
and further, it will indicate if they behave differently with respect
to the typestate.  In case a difference is detected, the
“non-determinism” is handled as explained later in this section.

The complete set of input symbols which would be declared and mapped
for the MediaPlayer class are setDataSource, prepare, prepareAsync, start, stop, reset,
release, and pause.



  
Callback instrumentation. As for the callin methods, which
act as the input symbols in the callback typestate, the callback methods
act as the output symbols in the callback typestate.
The developer specifies the set of output callback symbols and
associated snippets to detect when callbacks occur.
In most cases, this involved adding the listeners for the callbacks in
the initialization snippet as mentioned above. 
In the MediaPlayer class, the output symbols are onCompleted
and onPrepared.




 §.§ Automated Callback-Typestate Inference

Once the developer provides the input and output symbols
and the associated snippets, attempts to automatically learn the
callback typestate following the framework of the algorithm.



  
inference.
In , the learner tests sequences of inputs until she can form a
consistent hypothesis automaton.
Each such test (or sequence of inputs) is called a membership query.
Once a hypothesis automaton is produced, an equivalence query is
performed; i.e., the hypothesis automaton is checked for equivalence
with the true callback typestate.
If the two are equivalent, we are done; otherwise, a counter-example
test is returned from which the tool learns.
This process repeats until the produced hypothesis automaton is correct.

For MediaPlayer, the first set of membership queries each consist
of a single different callin.
Of these, only the query containing
setDataSource succeeds.  The learner continues with longer
membership queries while building the hypothesis automaton.  For
instance, it learns that prepareAsync and prepare do
not lead to the same state: it is possible to invoke the
start after prepare, but not after
prepareAsync.  Once the client receives the callback
onPrepared, start may be called.  The learner thus
hypothesizes a transition from the Preparing to the Prepared on onPrepared.  Once the hypothesis is
complete, the learner asks the equivalence query.
Initially, a counter-example to equivalence is returned using which
the learner refines its hypothesis.
The final solution is found after 5 equivalence queries.



  
Answering Equivalence Queries.
The equivalence query, i.e., checking if a learned callback typestate is
in fact the true callback typestate is undecidable in general.
However, assuming a bound on the size of the typestate, the equivalence
query can be implemented using further testing.
However, equivalence queries are still expensive and to make them
practical we present an new optimization based on a distinguisher
bound.
We can observe in Figure <ref> that for any pair of states there
is a transition in one state which leads to an error in the other.
This corresponds to a distinguisher bound of 1.
Small distinguisher bounds arise because typestates are not random
automata but part of an API designed for ease of use and robustness.
Such APIs are coded defensively and are fail-fast <cit.>, i.e.,
errors are not buffered but reported immediately.
Each state in the typestate has a specific function and an associated
set of callins and callbacks.
In automata terms, the alphabet is roughly the same size as the number
of states and each state has only a few transitions, making any two
states easy to distinguish.
In Section <ref>, we explain how to use the distinguisher
bound to implement equivalence queries and discuss why distinguisher
bounds are small in practice.



 §.§ Obstacles to Inference and Solutions

The based callback typestate inference algorithm makes several
assumptions about the behavior of the class that do not always hold.
is designed to detect these violations of assumptions and notify
the developer.
Here, we discuss two such assumptions, the exceptional situations that
arise when the assumptions are violated, and the additional developer
intervention needed to handle such cases.



  
Non-determinism.
In input-output automata learning theory, non-determinism makes
learning impossible.
Non-determinism is the possibility of the same sequence of
input callins producing different sequences of output callbacks across
tests.
Non-determinism may be due to various
controllable and non-controllable factors.
Controllable factors include cases where behavior depends on if a file
exists, if a URL is reachable, etc.
On the other hand, non-controllable factors include random number
generators, device sensors, etc.
In practice, most of the non-determinism was controllable.

The main technique for handling non-determinism is via refinement
of input or output alphabets.
Here, a single callin or callback is split into multiple "logical"
inputs or outputs.

  (a) Controllable non-determinism can be eliminated by incorporating
  the controlling factor into the inputs.
  For example, in the SQLiteOpenHelper class, the behavior of the
  constructor callin changes depending on if a file exists.
  However, after splitting the callin into two separate callins constructor/fileExists and constructor/noFileExists, the
  behavior of each of each callin becomes deterministic with respect to
  these callins.

  (b) Another source of non-determinism is when the same callback is
  used to notify logically different events.
  For example, a class may use a generic onComplete callback
  which is passed a status parameter that can have the values
  “Success” and “Failure”.
  Based on this value, different further callins are enabled, leading to
  non-determinism.
  Here, the developer may manually refine the callback into two output
  symbols onEvent/Success and onEvent/Failure, and the
  behavior is deterministic with respect to these.

In summary, for controllable non-determinism, the onus is on the
developer to identify the source of the detected non-determinism and
provide a refinement of the input or output alphabet and corresponding
code snippets to control the source.
No general technique exists to handle non-controllable non-determinism,
but specific cases can be handled using techniques shown in
Section <ref>.



  
Non-regularity.
Another basic assumption that based inference algorithm makes is
that the callback typestate under consideration is regular.
This assumption is commonly violated in request-response style behavior
of classes where the number of responses (output callbacks) invoked is
exactly equal to the number of requests (input callins).
Our solution to this problem is to restrict the learning to a subset of
the class behavior, such as inputs with at most one pending request
callin using a learning purpose <cit.>.
These restrictions makes the behavior regular and amenable to learning.




§ THE CALLBACK TYPESTATE LEARNING PROBLEM



We introduce formal models of interfaces, define the callback typestate
learning problem, and present an impossibility result about
learning typestates. Callback typestates have both inputs (corresponding
to callins) and outputs (corresponding to callbacks).
In automata theory, callback typestates can be seen as interface
automata.
Interface automata <cit.> are a well-studied model of automata that can
produce outputs asynchronously w.r.t. inputs.
We use the name callback typestates to emphasize that
they are a generalization of typestates as used in the programming
languages literature.



 §.§ Definitions and Problem Statement




  
Asynchronous interfaces.
Let  and  be the set of callins and
callbacks of an asynchronous interface.
We abstract away parameter and return values of callins and callbacks,
and model a behavior of the interface as a trace =
_0 …_n ∈ (∪)^*.
The interface  is given by
, , where ⊆{∪}^* is the prefix-closed set of all feasible
traces of the interface.



  In the android media-player example, one example of a trace is
  setDataSource() ·prepareAsync() ·onPrepared
  ·start() ·stop().





  
Interface automata.
We use interface automata <cit.> to represent asynchronous interfaces.
An interface automaton  is given by
, , , , _ where:
[(a)]

  *  is a finite set of states,

  * ∈ is the initial state,

  *  and  are finite sets of input and
  output symbols, and

  * _⊆×{∪}× are a set of transitions.

A trace  of  is given by
_0 …_n if ∃_0
…_n+1:
_0 = ∧∀ i.( _i, _i, _i+1) ∈_.
 is the set of all traces of .

We say that  models the
typestate of = , , if each trace of  is a trace of
, and vice versa.




  
Problem statement.
Given an interface = , ,,
the callback typestate learning problem is to learn an interface
automaton  such that =.
We allow the learner to ask a membership oracle
[] membership queries.
For a membership query, the learner picks
= _0 _1 …_n ∈^* and the membership
oracle [] returns either:
[(a)]

  * a trace ∈ whose sequence of callins is
  exactly , or

  *  if no such trace exists.




 §.§ The Theory and Practice of Learning Typestates




In general, it is impossible to learn callback typestates using only membership queries;
no finite set of membership queries fixes a unique interface
automaton.
However, callback typestates can be effectively learned given extra assumptions.
We now analyze the causes behind the impossibility and highlight the
assumptions necessary to overcome it.



  
Unbounded asynchrony.
Membership queries alone do not tell us if the interface will emit more outputs (callbacks) at any point in time.
Hence, we assume:

Assumption 1: Quiescence is observable.
This assumption is commonly used in ioco-testing frameworks <cit.>.
In our setting, we add an input  and an output
, where  is returned after a
 only if there are no other pending callbacks.
In practice,  can be implemented using
timeouts, i.e., pending callbacks are assumed to arrive
within a fixed amount of time.
If no callbacks are seen within the timeout,  is output.



  Using  and , in the MediaPlayer
  example, we have that setDataSource() ·prepareAsync()
  ·onPrepared ·wait ·quiet is a valid trace, but setDataSource() ·prepareAsync() ·wait ·quiet is
  not.




  
Behavior unboundedness.
For any set of membership queries, let k be the length of the longest query.
It is not possible to find out if the interface exhibits
different behavior for queries much longer than k.
This is a theoretical limitation, but is not a problem in practice <cit.>; most callback typestates are rather small (≤ 10 states).

Assumption 2: An upper bound on the size of 
the typestate being learned is known.



  
Non-determinism.
We need to be able to observe the systems' behaviors to learn them and non-determinism can prevent that.
Therefore, we assume:

Assumption 3: The interface is deterministic.
We assume that for every trace  of the interface,
there is at most one output ∈ such that ·∈.
In practice, the non-determinism problem is somewhat alleviated due to the nature of callback typestates (see Section <ref>).
See <cit.> for a detailed theoretical discussion of how non-determinism affects learnability.


  Consider an interface with traces given by (𝚒𝚗𝚙𝚞𝚝· ( 𝚘𝚞𝚝1|𝚘𝚞𝚝2 ))^*.
  All membership queries are a sequence of input's;
  however, it is possible that the membership oracle never returns any
  trace containing out2.
  In that case, no learner will be able to learn the interface exactly.





§ LEARNING CALLBACK TYPESTATES 
 USING 



Given Assumption 1 and Assumption 3, we first
build a “synchronous closure” of an
asynchronous interface (Section <ref>).
Then, we show how to learn the synchronous closure effectively given Assumption 2 (Section <ref> and <ref>).



 §.§ From Asynchronous to Synchronous Interfaces



Using Assumption 1 and 3, we build a synchronous version
of an interface in which inputs and outputs strictly alternate following <cit.>.
For synchronous interfaces, we can draw learning techniques from existing work <cit.>.

Define = ∪{} and =
∪{, , }.
The purpose of the extra inputs and outputs is discussed below.
For any ∈ (·)^*, we define
() = ∈ (∪)^* where
 is had from  by erasing all occurrences of
, , , and .



  
Synchronous closures.
The synchronous closure  of an asynchronous
interface = , , is given
by , , where  and
 are as above, and ⊆ (·)^* is defined as the smallest set satisfying the following:
  


    [        ϵ∈                    ;     ∈()·∈                 ··∈;     ∈()·∈                 ··∈;     ∈()·∉                 ··∈;    ∈∈()·∉                 ··∈; ∈ ends in                 ··∈ ]

  


Informally, in :
[(a)]

  * Each input is immediately followed by a dummy output
  ;

  * Each output is immediately preceded by a wait
  input ;

  * Any call to an input disabled in  is immediately
  followed by an .
  Further, all outputs after an  are 's.

  * Any call to  in a quiescent state is followed by
  .


Given [] and Assumption 1, it is easy to
construct the membership [].
Note that due to Assumption 3, there is exactly one possible reply
[]() for each query .
Further, by the construction of the synchronous closure, the inputs
and outputs in []() alternate.



  
Mealy machines.
We model synchronous interfaces using the simpler formalism of Mealy
machines rather than interface automata.
A Mealy machine  is a tuple  ,
, , , , where:
[(a)]

  * , , , and  are states,
  initial state, inputs and outputs, respectively,

  * : ×→ is a transition function, and

  * : ×→ is an output function.

We abuse notation and write (, _0…_n) =
_1…_n and (, _0…_n) =
'  if ∃_0,…, _n+1 : _0
= ∧_n+1 = ' ∧∀ 0 ≤ i ≤ n :
(_i, _i) = _i+1∧(_i,
_i) = _i.

A sequence _0_0…_n_n ∈ ( ·)^* is a trace of  if (,
_0…_n) = _0…_n.
We often abuse notation and write (_0…_n) instead of
(, _0…_n).
We denote by  the set of all traces of .





 §.§ : Learning Mealy Machines



For the sake of completeness, we describe the classical learning
algorithm by Angluin <cit.> as adapted to Mealy machines
in <cit.>.
A reader familiar with the literature on inference of finite-state
machines may safely skip this subsection.

Fix an asynchronous interface  and its synchronous closure
.
In , in addition to a membership oracle
[], the learner has access to an equivalence
oracle [].
For an equivalence query, the learner passes a Mealy machine  to
[], and is in turn returned:
[(a)]

  * A counterexample input = _0…_n
  such that = _0 …_n and
  []() ≠_0_0 …_n_n, or

  *  if no such  exists.



The full algorithm is in Algorithm <ref>.
In Algorithm <ref>, the learner maintains:
[(a)]

  * a set ⊆^* of state-representatives (initially set to {ϵ}),

  * a set ⊆^* of experiments
  (initially set to ), and

  * an observation table : (∪·) → (→^*).

The observation table maps each prefix  
and suffix  to
()(), where ()() is the
suffix of the output sequence of (·) of
length ||.
The entries are computed by the sub-procedure .

Intuitively,  represent Myhill-Nerode equivalence
classes of the Mealy machine the
learner is constructing, and  distinguish between
the different classes.
For  to form valid set of Myhill-Nerode classes, each
state representative extended with an input, should be equivalent to
some state representative.
Hence, the algorithm checks if each ·∈· is equivalent to some '
∈ (line <ref>) under ,
and if not, adds · to .
If no such · exists, the learner constructs a Mealy
machine  using the Myhill-Nerode equivalence classes, and queries
the equivalence oracle (line <ref>).
If the equivalence oracle returns a counterexample, the
learner adds a suffix of the counterexample to ;
otherwise, it returns .
For the full description of the choice of suffix,
see <cit.>.



  
  Let there exist a Mealy machine  with n states such that
   is the set of traces of .
  Then, given [] and [],
  Algorithm <ref> returns  making at most ||^2 n + || n^2 m membership and n
  equivalence queries, where m is the maximum length of
  counterexamples returned by [].
  If [] returns minimal counterexamples, m ≤
  O(n).




 §.§ An Equivalence Oracle Using Membership Queries



Given a black-box interface in practice, it is not feasible to directly
implement the equivalence oracle required for the algorithm.
Here, we demonstrate a method of implementing an equivalence oracle
using the membership oracle using the boundedness assumption (Assumption 2).
As before fix an asynchronous interface  and its synchronous
closure .
Further, fix a target minimal Mealy machine ^* such that ^*
is the set of traces of .



  
State bounds.
A state bound of  implies that the
target Mealy machine ^* has at most  states.
Given a state bound, we can replace an equivalence check with a number
of membership queries using the following theorem.

  
  Let  and ' be Mealy machines having k and k' states,
  respectively, such that ∃ w_i ∈^* : w_i≠'w_i'.
  Then, there exists an input word w_i' of length at most k + k' - 1 such
  that w_i'≠'w_i'.

The proof is similar to the proof of the bound k + k' - 2 for finite
automata (see <cit.>).
We can check equivalence of ^* and any given 
by testing that they have equal outputs on all inputs of length
at most k_ +  - 1, i.e., using O(||^ + k - 1) membership queries.



  Fix a state bound of  for the target Mealy machine
  ^*.
  Given a membership oracle [] and a Mealy machine
   with k states, the equivalence query can be answered using at
  most ||^ + k - 1 membership
  queries.


While this simple algorithm is easy to implement, it is
inefficient and the number of required membership queries make it
infeasible to implement in practice.
Other algorithms based on state bounds have a similar problems with
efficiency (see Remark in Section <ref>).
Further, the algorithm does not take advantage of the structure of
.
The following discussion and algorithm rectifies these short-comings.



  
Distinguisher bounds.
A distinguisher bound of ∈
implies that for each pair of states _1^*, _2^* in the
target Mealy machine ^* can be distinguished by an input word w_i
of length at most , i.e.,
^*(_1^*, w_i) ≠^*(_2^*, w_i).
Intuitively, a small distinguisher bound implies that each state
is “locally” different, i.e., can be
distinguished from others using small length input sequences.

The following theorem shows that a state bound implies a comparable
distinguisher bound.

  
    State bound k implies distinguisher bound k - 1.




  
Small distinguisher bound.
In practice, distinguishers are much smaller than the bound implied by the state bound.
For the media-player, the number of states is 10, but only distinguishers of length 1 are required.
This pattern tends to hold in general due to the following principles of good interface design:

  
  * Clear separation of the interface functions.
        Each state in the interface has a specific function and a specific set of callins and callbacks.
        There is little reuse of names across state.
        The typestate's alphabet is roughly the same size as the number of states.
  
  * Fail-fast.
        Incorrect usage of the interface is not silently ignored but reported as soon as possible.
        This makes it easier to distinguish states as disabled callins
        lead directly to errors.
  
  * No buffering.
        More than just fail-fast, a good interface is interactive and the effect of callins must be immediately visible rather than hidden.
        A good interface is not a combination lock that requires many
        inputs that are silently stored and only acknowledged at the very end.

This observation also is not specific to callbacks typestates and it has been already observed for libraries <cit.>. 



  
Equivalence algorithm.
Algorithm <ref> is an equivalence oracle for Mealy
machines using the membership oracle, given a distinguisher bound.
First, it computes state representatives
: →^*:
for each ∈, (,
()) = (line <ref>).
Then, for each transition in , the algorithm first checks whether
the output symbol is correct (line <ref>).
Then, the algorithm checks the “fidelity” of the transition up to the
distinguisher bound, i.e., whether the representative of the previous
state followed by the transition input, and the representative of the
next state can be distinguished using a suffix of length at most
.
If so, the algorithm returns a counterexample.
If no transition shows a different result, the algorithm returns .

Two optimizations further reduce the number of membership queries:
[(a)]

  * Quiescence transitions.
  Transitions with input  and output  need
  not be checked at line <ref>; it is a no-op at the
  interface level.

  * Error transitions.
  Similarly, transition with the output  need not be
  checked as any extension of an error trace can only have error
  outputs.


  * Representative transitions.
  If ()· = (')
  at line <ref>, we once again need not check
  the transition.
  Using state representatives from instead of
  computing them at line <ref> usually leads to a
  larger number of such cases.





  Note that if Algorithm <ref> is being called
  from Algorithm <ref>, the state representatives from can be used instead of recomputing R in
  line <ref>.
  Similarly, the counterexample analysis stage can be skipped in the
  algorithm,
  and the relevant suffix
  can be directly returned ( in lines <ref>
  and <ref>; and  in line <ref>).






  
  Assuming the distinguisher bound of  for the
  target Mealy machine ^*, either
  [(a)]
  
  * Algorithm <ref> returns  and
    ∀ w_i ∈^*: (w_i) = ^*(w_i), or
  
  * Algorithm <ref> returns a
    counterexample  and ≠^*.
  
  Further, it performs at most ||·||^ + 1 membership queries.



Algorithm <ref> and
Theorem <ref> give us improved complexity for
state bounds.

  Assuming a state bound , equivalence checking for a
  Mealy machine can be implemented using at most ||·||^ membership queries.




  
  Note that the problem being addressed here, i.e., testing the
  equivalence of a given finite-state machine and a system whose
  behavior can be observed, is equivalent to the conformance testing
  problem from the model-based testing literature.
  However, several points make the existing conformance testing
  algorithms unsuitable in our setting.

  Popular conformance testing algorithms, like the
  W-method <cit.> and the W_p-method <cit.>, are based
  on state bounds and have an unavoidable O(||^) factor in the complexity.
  In our experiments, the largest typestate had 10 states and 7
  inputs.
  The O(||^) factor leads to an
  infeasible (i.e., > 10^8) number of membership queries.
  However, since distinguisher bounds are often much smaller than state
  bounds, O(||^)
  membership queries are feasible (i.e., 10^3).
  The W- and W_p-methods cannot directly use
  distinguisher bounds.

  The other common algorithm, the D-method <cit.>,
  does not apply in our setting either.
  The D-method is based on building a distinguishing sequence,
  i.e., an input sequence which produces a different sequence of
  outputs from every single state in the machine.
  However, for callback typestates, such single distinguishing
  sequences do not exist in practice.
  For similar reasons, conformance testing algorithms such as the
  UIO-method <cit.> do not apply either.

  In this light, we believe that Algorithm <ref>
  is a novel conformance testing algorithm useful in specific settings
  where resets are inexpensive and systems are designed to have
  small distinguisher bounds.




 §.§ Putting It All Together


We now present the full callback typestate learning solution.


  Given a deterministic interface  with
  observable quiescence and the membership oracle
  [].
  Assume there exists an interface automaton
   with n states with distinguisher bound
   modeling the typestate of .
  Interface automaton  can be learned with
  O(||· n^3 + n ·||^) membership queries.




  
Proof sketch.
Starting with an asynchronous interface  and a membership
oracle [], using Assumption 1 and
Assumption 3 we can construct the membership oracle
[] for the synchronous closure  of
.
Given the distinguisher bound (or a state bound using Assumption
2 and Theorem <ref>), we can construct an equivalence
oracle [] using
Algorithm <ref>.
Oracles [] and [] can then be
used to learn a Mealy machine  with the same set of traces as
.
This Mealy machine can be converted into the interface automata
representing the callback typestate of  by:
[(a)]

  * Deleting all transitions with output  and all
  self-loop transitions with output , and

  * Replacing all transitions with input  with the
  output of the transition.




§ ACTIVE LEARNING FOR ANDROID



We implemented our method in a tool called .
In this section we describe how it works, the practical challenges we faced when working with Android, and our solutions to overcome them.
is implemented as an Android application and learns callback
typestates from within a live Android system.



 §.§ Designing an Experiment


To learn a typestate, a user creates a test configuration (an
extension of the LearningPurpose class) providing necessary
information about a Java class under study.

If known, the distinguisher bound can be provided here directly;
otherwise, it can be obtained from Assumption 2 by
Theorem <ref>.

The instrumented alphabet, also defined here, specifies an
abstract alphabet for the learning algorithm and translation between
the abstract alphabet and concrete callins/callbacks of the
class under study.

Several other options are available for adjusting the learning, the
most important being the quiescence timeout which determines
Assumption 1.



 §.§ Observing Asynchronous Callbacks


In our approach we assume bounded asynchrony (Assumption 1) and, therefore, we can
observe when the interface does not produce any new output (quiescence).
We enforce this assumption on a real system with timeouts:
the membership query algorithm waits for a new output for a fixed amount
of time , assuming that quiescence is reached when this time is elapsed.
However, Android does not provide any worst case execution time for
the asynchronous operations and we rely on the user to choose a large enough .

The membership query also assumes the existence of a minimum time  before a callback occurs.
This ensures that we can issue a membership query with two consecutive callins (so, without a  input in between), i.e., we have the time to execute the second callin before the output of the first callin.

Consider the MediaPlayer example from
Section <ref>.
The membership query setDataSource(URL) ·
·prepareAsync · may not return the
onPrepared if  is violated, i.e., if the callback
does not arrive before the timeout, and while testing it is possible that the prepareAsync ·start might not return an error as expected if the lower bound  is violated.

To avoid such issues we try to control the execution environment and parameters to ensure that callbacks occurred between  and .

In the MediaPlayer case, we must pick the right media source file.




 §.§ Checking and Enforcing Our Assumptions


The simplest experiment to learn a class's callback typestate ties a single input symbol to each of its callins and a single output symbol to each of its callbacks.
However, many Android classes have behaviors which cause this simple experiment to fail and require more detailed experiments to succeed.

The main challenges when designing an experiment are
[(a)]

  * Non-deterministic behaviors, i.e., the state of the device
  and external events may influence an application. These elements are inherently
    non-deterministic; however, non-determinism violates Assumption 3.

  * The parameter space required to drive concrete
  test cases to witness a membership query is potentially infinite.
  Though we have ignored callin parameters till now, they are a
  crucial issue for testing.

  * The protocol we are learning may not be a regular language.
  Note that this is a violation of Assumption 2.




  
Non-Deterministic Behavior.
Non-deterministic behavior is disallowed by our Assumption 3.
However, to make this assumption reasonable we must make non-determinism straightforward to eliminate when it arises.
We explain two primary classes of non-deterministic behaviors and strategies to eliminate these behaviors.
The first class is related to controllable inputs and the second to
uncontrollable ones (such as inputs from the device sensors).

Because the learning algorithm cannot learn from non-deterministic
systems, will terminate if such behavior is detected. To assist in this process, will report a non-deterministic behavior is
detected and display the disagreeing
sequences to the user.
It detects this by caching all membership queries as input/output sequence pairs.
When a new trace is explored, checks that the trace prefixes are compatible with the previously seen traces.

In the first case, a hidden (not modeled) controllable input
influences the typestate.
We resolve this non-determinism by manually adding the input value and
create a finer alphabet that explicate the previously hidden state of
the environment.

For example, in the class SQLiteOpenHelper, the getReadableDatabase() may either trigger a onCreate callback or
not, depending on the parameter value to a previous callin (constructor)was the name of an existing database file.
Hence, the behavior of the callin is non-deterministic, depending on the
status of the database on disk.

In the SQLiteOpenHelper example, we split the constructor callin into constructor/fileExists and constructor/noFileExists and pass the right parameter values in each
case.

With this extra modeling we can learn the interface automaton, since the
execution getReadableDatabase() ends in two different states of the
automaton (see Figure <ref>).


The second class is the effect of the uncontrollable inputs on a
typestate.
Such effects, by definition, cannot be controlled or made explicit prior to the call.
We can sometimes to remove this non-determinism by merging different
outputs, considering them to be the same.
This is the dual of the previous solution.

An example is the SpeechRecognizer, for which calling startListening produces different callbacks depending on the environment.
As the environment cannot be reasonably controlled, we merge outputs to go to the same state.
If outputs are erroneously merged, the non-determinism will propagate and continue to manifest.
Thus there is no risk of unsound results. 



  
Handling Callin Parameters.
While parameter-less callins such as start and stop are common in Android classes, many parameterized callins exist.
Because input symbols need to be listed in the experiment definition, the full range of parameter values cannot be explored.
In practice, we found that parameters often have little effect on the typestate automaton.
In cases where they do affect the automaton, multiple input symbols can be defined to represent the same method called with several different parameters.
This solution is similar to splitting on environmental effects when dealing with non-determinism.



  
Learning from Non-Regular Languages.
An intrinsic limitation of is that it learns only regular languages.
However, some classes expose non-regular protocols.
Common cases include situations where a request callin invoked
n times trigger exactly n response callbacks.
In the SpellCheckerSession class, callin getSuggestion and callback onGetSuggestions follow this pattern.

However, even in such cases, it can be useful to build a regular approximation of the typestate.
For example, restricting the typestate to behaviors where there is at most one pending request (a regular subset) provides all the information a programmer would need.
Hence, in such cases, we use the technique of learning purposes <cit.> to learn a regular approximations of the infinite typestate.




§ EMPIRICAL EVALUATION



We evaluated our interface-learning technique, as implemented in
, by using it to generate callback typestates for 16 classes,
sampled from the Android Framework and popular third-party libraries.
is available at .
For these experiments, was run on an LG Nexus 5 with Android
framework version 23.  Our evaluation was designed to answer the
following questions:



  * Does our technique learn typestates efficiently?

  * What size distinguisher bounds occur in practice?  Do they
  support the small distinguisher bound hypothesis?

  * Do the callback typestates we learn reveal interesting or
  unintended behavior in the interfaces?




  
Methodology.
For each experimental class, we manually identified a reduced alphabet
of relevant callins and callbacks and provided them (along with other
necessary information as explained in Section <ref>) to
through instances of the LearningPurpose.

Relevant callins and callbacks for these experiments were those which,
according to the available documentation, appeared to trigger or
depend on typestate changes (enabling or disabling of parts of the
interface).

Each instance consisted of 50-200 lines of, mostly boiler-plate,
Java or Scala code.

To evaluate efficiency, we measured the overall time taken for
learning, as well as the number of membership (MQ) and equivalence
queries (EQ).  The number of queries is likely a better measure of
performance than running time: the running time depends on external
factors.  For example, in the media player the running time depends on
play-length of the media file chosen during testing.

We validated the accuracy of learned callback typestates using two
approaches.  First, for classes whose documentation contains a picture
or a description of what effectively is an callback typestate, we
compared our result to the documentation.  Second, for all other
classes we performed manual code inspection and ran test apps to
evaluate correctness of the produced typestates.

We used a distinguisher bound of 2 for our experiments; further, we
manually examined the learned typestate and recorded the actual
distinguisher bound.  For our third question, i.e., does the learned
callback typestate reveal interesting behaviors, we manually examined
the learned typestate, compared it against the official Android
documentation, and recorded discrepancies.





 §.§ Results

We discuss the results (in Table <ref>) and
our three questions.

Question 1: Efficiency.  The table shows that our
technique is reasonably fast: most typestates learned within a few
minutes.  The longest one takes 71 minutes, still applicable to
nightly testing.  The numbers for membership queries are reported as
X (Y)—X is the number of membership queries asked by the
algorithm, while Y is the number actually executed by the membership
oracle.  This number is lower as the same query may be asked multiple
times, but is executed only once and the result is cached.

For each benchmark, the accuracy validation showed that the
produced typestate matched the actual behavior.

Question 2: Distinguisher Bounds.  As mentioned
before, we used a distinguisher bound of 2 for all experiments.
However, a manual examination of the learned callback typestates
showed that a bound of 1 would be sufficient in all
cases except the SQLiteOpenHelper and the OkHttpCall
where bounds of 2 are necessary.  This supports our conjecture that,
in practice, interfaces are designed with each state having a unique
functionality (see Section <ref>).

Question 3: Interesting Learned Behavior.
Of the three questions, our experiments to examine the learned
callback typestate for interesting behavior turned out to be the
most fruitful, uncovering several discrepancies, including corner cases,
unintended behavior and likely bugs, in the Android framework.
These results reaffirm the utility of our main goal of automatically
learning callback typestate, and suggest that learning typestate can
serve valuable roles in documentation and validation of callback
interfaces.

In 2 cases, the learned typestate and documented behavior differed in
certain corner cases.
We carefully examined the differences, by framework
source examination and manually writing test applications, and found
that the learned typestate was correct and the documentation
was faulty.
In 5 other cases, we believe the implemented behavior is not the
intended behavior, i.e., these are likely bugs in the Android
implementation.

These discrepancies mostly fall into two separate categories:

Incorrect documentation.
In such cases, it turned out that the discrepancy is minor and unlikely to
produce bugs in client programs.

Race conditions.
Several likely bugs were due to a specific category of race conditions.
These interfaces have
[(a)]

  * a callin to start an action and a corresponding callback which
  is invoked when the action is successfully completed;

  * a callin to cancel an already started action and a corresponding
  callback which is invoked if the action is successfully cancelled.

When the start action and cancel action callins are called in sequence, the
expectation is that exactly one of the two callbacks are called.
However, when the time between the two callins is small, we were able to
observe unexpected behaviors, including neither or both callbacks being
invoked.



 §.§ Selected Experiments

Of our 16 benchmarks, we briefly explain 5 here.  The remaining experiments are discussed in the technical report <cit.>[<http://arxiv.org/abs/1701.07842>].

MediaPlayer
This is the class from the example in
Section <ref>.
The learned typestate differs from the existing documentation.
The learned typestate:
[(a)]

  * has the pause callin enabled in
  the “playback completed” state, and

  * shows that onPrepared is
  invoked even after the synchronous callin prepare.

Though undocumented, these behaviors are unlikely to cause any issues.


AsyncTask
The AsyncTask class turns arbitrary computations into callback operations
with progress tracking and results are delivered via callbacks.  For our
experiment, the computation is a simple timer.  A constructed AsyncTask object
performs its task when it receives the execute callin, and then
either returns the results
with the
onPostExecute callback, or returns an onCancelled if
cancel is called first.  The object is single-use; after it has
returned a callback it will accept no further execute commands.

Our experiment revealed an unexpected edge-case: if execute
is after cancel but before the onCancelled
callback is received, it will not throw an exception but will never
cause the callback task to be run.  The learned interface is
in Figure <ref>.



SpeechRecognizer 
This class provides an example of uncontrollable environmental
non-determinism.  The particular callback that signals the end of the
speech session—either an onResults or an onError—is determined by the environment (in particular, the sound
around the phone during the test).  In this case, to reduce the system
to a deterministic one we can learn, we supposed that the state after
an onResults or onError is the same and merged
the two callbacks into a single onFinished symbol.

Our results revealed two interesting corner cases for the ordering
of inputs.  First, if an app calls cancel between
calling startListening and receiving the onReadyForSpeech callback (represented by our “starting”
output symbol), calling startListening again will have
no effect until after a certain amount of time, as shown by the
wait transition from state “Cancelling” to “Finished”.
Delays in readiness like this can be generally considered bugs; if a
system will not be ready immediately for inputs it should provide a
callback to announce when the preparations are complete, so as not
to invite race conditions.

Our second corner case is where the app calls stopListening as the very first input on a fresh
SpeechRecognizer.  This will not throw an exception, but calling
startListening at any point after will fail, making the
object effectively dead.

SQLiteOpenHelper This class provides a more structured
interface for apps to open and set up SQLite databases.  It has
callbacks for different stages of database initialization,
allowing apps to perform setup operations only as they are needed.
When a database is opened with getWritableDatabase, a
callback onConfigure is called, followed by an
onCreate if the database didn't exist yet or an
onUpgrade if the database had a lower version number
than was passed to the SQLiteOpenHelper constructor, all followed
finally by an onOpen when the database is ready for
reading.  The database can then be closed with a close.

Our experiment observed the callbacks when opening
databases in different states (normal, non-existent, and out of
date) and performing the  operation at different
points in the sequence.  We found that once the
 method is called, calling
 will not prevent the callbacks from being run.


VelocityTracker

This class was a special case with no asynchronous behavior; it was a
test of our tool's ability to infer traditional, synchronous
typestates.

The class has a recycle method that we expected to disable
the rest of the interface, but our tool found (and manual tests
confirmed) that the other methods can still be called after recycling.

The documentation's warning that “You must not touch the object after
calling [recycle]” is thus not enforced.



§ RELATED WORK



Works which automatically synthesize specifications of the valid
sequences of method calls
(e.g. <cit.>)
typically ignore the asynchronous callbacks.

Static analysis has been successfully used to infer typestates
specifications (importantly, without callbacks) <cit.>.

The work in <cit.> infers classical typestates for Java classes
using .

In contrast, our approach is based on testing.  Therefore, we
avoid the practical problem of abstracting the framework code. On the
other hand, the use of testing makes our oracles
sound only under assumptions.
Similarly,  <cit.> uses to infer classical
typestates, including ranges of input parameters that affect
behavior. However, their tool is based on symbolic execution,  and thus
would not scale to systems as large and complex as the Android
Framework.


Inferring interfaces using execution traces of client programs using
the framework is another common
approach <cit.>.

In contrast to dynamic mining, we do not rely on the
availability of client applications or a set of execution traces.
The algorithm drives the testing.

The analysis of event-driven programming frameworks has recently
gained a lot of attention (e.g.
 <cit.>).

However, none of the existing works provide an automatic approach to synthesize
interface specifications.

Analyses of Android applications mostly focus on either statically proving
program correctness or security
properties <cit.>
or dynamically detecting race
conditions <cit.>.  These
approaches manually hard-code the behavior of the framework to increase the precision of the analysis.

The callback typestate specifications that we
synthesize can be used here, avoiding the manual
specification process.


Our work builds on the seminal paper of Angluin <cit.> and
the subsequent extensions and optimizations. In particular, we build on
for  I/O automata <cit.>. The
optimizations we use include the counterexample suffix analysis
from <cit.> and the optimizations for prefix-closed
languages from <cit.>.
The relation to conformance testing methods <cit.> has been discussed in Section <ref>.





§ CONCLUSION



We have shown how to use active learning to infer callback typestates. We
introduce the notion of distinguisher bound which take advantage of good
software engineering practices to make active learning tractable on the Android
system. Our method is implemented in the freely available tool called .
This paper enables several new research directions. We plan to
investigate mining parameters of callins from instrumented trace from real user interactions, as well as the inference of structured typestates (for instance, learning a typestate as a product of simpler typestates).




This research was supported in part by DARPA under agreement
FA8750-14-2-0263.

Damien Zufferey was supported in part by the European Research Council Grant
Agreement No. 610150 (ERC Synergy Grant ImPACT
(<http://www.impact-erc.eu/>)).



plain


