Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II
Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II
复制标题
计算机辅助验证 - 第 30 届国际会议，CAV 2018，作为联邦逻辑会议的一部分举行，FloC 2018，英国牛津，2018 年 7 月 14-17 日，会议记录，第二部分
DOI：
10.1007/978-3-319-96142-2_29
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Chen T
中科院分区：
文献类型：
--
作者：
Chen T
在本文中，我们提出了Android堆栈机（ASM），一个正式的模型来捕捉Android多任务的关键机制，如活动，回栈，启动模式，以及任务的亲和力。该模型基于具有多个堆栈的下推系统，重点关注Android系统在与携带特定启动模式和任务亲和力的Activity交互时回栈的演变。在形式化分析方面，我们研究了ASM的可达性问题。虽然一般的问题被证明是不可判定的，我们确定的表达片段，下推系统或其扩展的各种验证技术被利用来显示问题的可判定性。
In this paper, we propose Android Stack Machine (ASM), a formal model to capture key mechanisms of Android multi-tasking such as activities, back stacks, launch modes, as well as task affinities. The model is based on pushdown systems with multiple stacks, and focuses on the evolution of the back stack of the Android system when interacting with activities carrying specific launch modes and task affinities. For formal analysis, we study the reachability problem of ASM. While the general problem is shown to be undecidable, we identify expressive fragments for which various verification techniques for pushdown systems or their extensions are harnessed to show decidability of the problem.