毕业设计外文资料翻译--Android应用程序验证

《毕业设计外文资料翻译--Android应用程序验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、毕业设计外文资料翻译学院：专业班级：学生姓名：学号：指导教师：外文出处：(外文)H.v.d.Merwe“VerificationofAndroidApplications”2015IEEE/ACM37thIEEEInternationalConferenceonSoftwareEngineering附件：1.外文资料翻译译文；2.外文原文指导教师评语：原文所涉及内容与课题有较好的关联，翻译难度适中。该生所作的译文，术语的使用基本准确，译文内容与原文含义基本相符，但部分译文语句不是很通顺。译文格式符合规

2、范，按时完成了下达的外文翻译任务。签名：年月日1．外文资料翻译译文Android应用程序验证摘要本研究探讨了另一种用模型检测的方法来分析Android应用程序。我们开发了名为JPF－Android的一个扩展的Java路径查找器(JPF)验证Android平台之外的Android应用程序。JPF是一个强大的Java模型检查和分析引擎，对检测其使用细粒度分析能力角落情况和难以发现的的错误非常有用。JPF－Android提供了一个可以在Android应用程序框架上运行的Android应用程序，它可以产生输入

3、事件或分析含有输入事件序列驱动的应用程序的执行输入脚本。JPF－Android通过模拟这些输入事件遍历应用程序的所有执行路径，并可以检测常见的侵权行为如Android程序运行时的死锁或者异常。它还引入了用户定义的执行规范要求的清单来检验应用程序的执行流程。一、介绍许多外部引用和依赖关系的软件应用是众所周知的难以分析和验证。这些外部依赖关系构成应用程序的执行上下文的一部分，也被成为应用程序的环境。对于应用在分析过程中的正确的执行，可适应，受控环境，反应要求准确并且一致性。运行中的Android程序构成一

4、个组，因为它们有许多外部引用和依赖关系。Android应用的环境由安卓软件堆栈组成，其中内部有一个客户端-服务器设计(图1)。该应用程序构建于Android应用程序框架的顶部。该框架提供了一个应用，包括事件处理和处理的核心实现，应用组件和资源管理以及进程间通信(IPC)促进其他应用程序和系统服务。设备上的所有应用程序的状态是由系统服务器控制的。系统服务器包含一组共享的服务，例如窗口管理器、包管理器以及控制每个应用程序组件运行状态的活动管理器。Android应用程序是由输入事件从系统服务和其他应用程序驱

5、动的。这些事件包括用户界面(UI)和通过系统服务器发送到相应的应用程序的系统事件。Android的应用环境分析工具面临三大挑战：(1)Android应用程序都严重依赖Android应用框架，并且系统服务不可以运行在软件堆栈之外，(2)由于Android应用程序有许多切入点异步设计，分析需要一个驱动程序来执行应用程序，(3)由于异步、多线程设计以及应用程序的使用以及反射和本机方法的使用，很难对应用程序的流或执行进行可靠的检测。如果应用程序在软件栈上执行，验证执行更是挑战，因为软件需要被编辑或重新编译或表

6、明每个版本的Android系统。图1安卓环境目前常用来分析Android应用程序的方法有动态和静态分析。静态分析通常需要测试下的系统被编译(不运行)，因此不需要生成测试驱动程序。然而，静态分析仍然需要模拟本机代码和隐式依赖关系，以及指定属性来检查(例如，内存泄漏，空指针异常，具体的使用模式)。结果通常是一个近似的，但Android应用程序错误可能是由于在其上运行应用程序的工具需要的模型被错过。静态分析也不可能向用户提供为了进行验证导致事件可能出现的问题的序列。相反，动态分析需要测试下的系统是可运行的，

7、需要生成测试驱动程序。此外，单元测试需要生成模仿对象。这种类型的测试使用的测试预言和断言是为了保证组件的正确运行。动态分析提供了应用程序的一个欠近似分析，其主要的挑战是产生获得令人满意的的应用程序代码的覆盖的输入事件。模型检验是一种成熟的检验技术，可以用来证明如果状态空间是(足够小)有限的，那么在应用程序上是不存在性能错误的。然而，最常见的是被用于找到简单的错误，即使是在状态控件是无限的情况下。搜索空间使用状态匹配和回溯而动态执行关闭应用而减少的。即使状态匹配，模型检查具有从状态空间爆炸的问题，并且实

8、际环境往往是抽象的而减少状态空间。由于模型检查需要细粒在应用程序的执行控制，对环境的适应性和可定性的模型是必需的。对于这项研究，我们着重核查使用一般的Java应用程序开发的验证工具验证Android应用程序。更具体的讲，我们扩展JPF，一个强大的模型检查和分析引擎，验证和分析Android应用程序。我们使用JPF，因为它是Java应用程序开发，它可以应用到Android程序(如符号路径查找器)很多扩展。由于Android应用程序是动态执行的，我们面临和一