一句话：提出回调 typestate 概念，用有限状态机刻画 Android 异步组件交互协议，并指出规格编写困难。
Android 等事件驱动编程框架由具有异步接口的组件构成。与这些组件交互的协议通常可由有限状态机描述，作者将这类规范称为 callback typestate（回调 typestate）。它类似经典 typestate，但区别在于其输出（callback）是异步产生的。此类规范虽有用，却因编写困难、容易出错而并不常见。摘要未给出具体方法、工具实现或实验评估；标题中的 DroidStar 可能指作者为此提出的系统或工具，但摘要未展开。
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.
DOI 原文 ·
@inproceedings{paperbot4452,
title = {D
<scp>roid</scp>
S
<scp>tar</scp>},
author = {Arjun Radhakrishna and Nicholas V. Lewchenko and Shawn Meier and Sergio Mover and Krishna Chaitanya Sripada and Damien Zufferey and Bor-Yuh Evan Chang and Pavol Černý},
booktitle = {ICSE},
year = {2018},
doi = {10.1145/3180155.3180232}
}