ausblenden:
Schlagwörter:
Computer Science, Logic in Computer Science, cs.LO,Computer Science, Learning, cs.LG,Computer Science, Programming Languages, cs.PL
Zusammenfassung:
In event-driven programming frameworks, such as Android, the client and the
framework interact using callins (framework methods that the client invokes)
and callbacks (client methods that the framework invokes). The protocols for
interacting with these frameworks can often be described by finite-state
machines we dub *asynchronous typestates*. Asynchronous typestates are akin to
classical typestates, with the key difference that their outputs (callbacks)
are produced asynchronously.
We present an algorithm to infer asynchronous typestates for Android
framework classes. It is based on the L* algorithm that uses membership and
equivalence queries. We show how to implement these queries for Android
classes. Membership queries are implemented using testing. Under realistic
assumptions, equivalence queries can be implemented using membership queries.
We provide an improved algorithm for equivalence queries that is better suited
for our application than the algorithms from literature. Instead of using a
bound on the size of the typestate to be learned, our algorithm uses a
*distinguisher bound*. The distinguisher bound quantifies how two states in the
typestate are locally different.
We implement our approach and evaluate it empirically. We use our tool,
Starling, to learn asynchronous 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 Starling learns asynchronous
typestates accurately and efficiently. Additionally, in several cases, the
synthesized asynchronous typestates uncovered surprising and undocumented
behaviors.
