摘要
为分析安卓应用回调函数的时序调用关系,提出一种全局、细粒度的回调函数建模方法,涵盖对生命周期、非生命周期及不同类型组件间的回调函数处理,关注回调序列上的注册对象定义及操作。利用模型检测语言NuSMV表征生成的回调序列,LTL (linear temporal logic)表示目标验证属性,得以自动化地验证应用缺陷。通过设计一个移动应用回调排序原型系统SQDroid,并将该系统应用在数据竞争缺陷检测上,验证了该方法的有效性。
To provide a sequential call analysis between callback functions in Android application,aglobal and fine-grained model for callback functions was proposed.The callback functions among life cycle,non-life cycle and different types of components were addressed.The definitions and operations of registration object of callback sequence were also contained.The callback sequences were generated using the model detection language NuSMV,and the target verification attribute was represented by the LTL(linear temporal logic),so the defects could be verified automatically.A mobile application callback sequencing prototype system SQDroid was designed to detect data competition flaws.The validity of the method is demonstrated.
作者
崔洁
陈亮
康介恢
吴彦峰
于家伟
CUI Jie;CHEN Liang;KANG Jie-hui;WU Yan-feng;YU Jia-wei(Electric Power Research Institute,State Grid Tianjin Electric Power Company,Tianjin 300384,China;College of Computer and Control Engineering,Nankai University,Tianjin 300350,China)
出处
《计算机工程与设计》
北大核心
2019年第1期218-222,235,共6页
Computer Engineering and Design
基金
天津市自然科学基金重点基金项目(17JCZDJC30700)
