Android 堆栈机模型

Taolue Chen, Jinlong He, Fu Song, Guozhen Wang, Zhilin Wu, Jun Yan (2018): Android Stack Machine. CAV 2018: 487-504

背景：Android是Google公司开发的智能手机开源操作系统，月活跃用户超过20亿，目前市场份额最大（超过60%），而且Android应用市场Google Play有超过350万的应用程序。Android多任务机制是Android平台的一种重要的机制，其通过活动（Activity）和回退栈（Back stack）的独特设计，极大地方便了用户操作，比如用户可以非常方便地进行应用切换，或者极其平滑地浏览历史。

科学难题：Android多任务机制比较复杂，是一个栈中有栈的两层嵌套结构，开发人员很难准确理解。在一些著名的问答网站（比如Stack Overflow上）就有很多与Android多任务机制相关的问题，甚至Android的官方文档对其的描述和介绍都比较模糊。对Android多任务机制的语义进行形式化建模，可以帮助开发人员准确理解Android多任务机制。而由于Android多任务机制的栈中有栈的嵌套结构，根据Android多任务机制的形式语义对Android应用的多任务行为进行静态分析和验证，是一个很有挑战性的问题。

重要突破：我们对Android的多任务机制进行了形式建模，考虑了多任务机制中活动的两种最基本的属性（即启动模式和任务亲和力），提出了Android Stack Machine（ASM）的形式模型，通过实验证实了ASM和Android平台实际运行结果的一致性。进一步地，我们对于ASM的可达性问题进行了研究，证明了其可达性问题一般是不可判定的，但是对于一类能涵盖很多实际App的子模型，其可达性问题是可判定的。我们的判定算法使用下推系统的带转换器的扩展来计算多栈的有限状态抽象，将可达性问题转换为下推系统的可达性问题。