安卓应用的回调序列与模型检测应用

摘要：

为分析安卓应用回调函数的时序调用关系, 提出一种全局、细粒度的回调函数建模方法, 涵盖对生命周期、非生命周期及不同类型组件间的回调函数处理, 关注回调序列上的注册对象定义及操作.利用模型检测语言NuSMV表征生成的回调序列, LTL (linear temporal logic) 表示目标验证属性, 得以自动化地验证应用缺陷.通过设计一个移动应用回调排序原型系统SQDroid, 并将该系统应用在数据竞争缺陷检测上, 验证了该方法的有效性.

关键词：Android应用、回调函数、模型检测、缺陷检测、数据竞争

所属期刊栏目：40

分类号：TP311.52(计算技术、计算机技术)

资助基金：天津市自然科学基金重点基金项目17JCZDJC30700

在线出版日期：2019-05-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：218-222,235