Android操作系统基于Linux2.6内核,采用“应用程序关闭而不退出”的设计概念,即应用程序将会常驻内存,此外,不同于Linux操作系统,Android操作系统并未采用页面交换机制,即物理内存大小等于实际可用内存大小。在国内外与Android相关的论坛中,最常被讨论的问题就是Android手机操作系统内存紧张应用程序无法安装或应用程序崩溃等问题。本文围绕着Android“应用程序关闭而不退出”的设计理念,研究了Android操作系统内存管理机制,通过形式化规范与形式化验证的方法,重点分析了Android操作系统的内存回收机制。针对本文所研究课题的特殊性,在已有操作系统实现源码,并缺乏功能需求文档的基础上进行形式化分析,故本文采取有别于传统的形式化分析方法中逐层精华的步骤,首先从官方设计说明文档和API文档,以及Android操作系统源代码的注释部分抽取相应的规范性质。随后按照两种技术路线来进行形式化分析。路线一：使用规范语言进行抽象,建立分层的形式化规范。首先使用与具体程序设计语言特性无关的Larch语言族的共享语言(简称LSL)来进行性质及函数规范的初步描述。然后将LSL规格说明书分别转换为支持Java语言特性的Java建模语言(简称JML)形式化规范和支持C语言特性的并发C验证语言(简称VCC)形式化规范。并在此基础上应用定理证明等手段,验证提取出的Android操作系统内存管理相关部分的Java代码及C代码是否符合形式化规范。路线二：使用通信顺序进程语言(简称CSP),从内存、进程、操作系统,及内存回收算法四个方面,对Android操作系统内存管理建立形式化的系统并发模型。并抽取系统属性,用模型检测的方法来验证系统模型是否满足属性。对于两种路线验证或检测出的问题采用控制流图分析,等价类分析和程序模拟等辅助手段,深入分析其原因,予以解释,并给出问题出现的场景描述。