摘要: 1、研究背景（context）
上下文精化关系是一种重要的可组合地验证并发对象功能正确性的方法。因为它拥有可以灵活地为并发对象定义出不同粒度的抽象规范并进行验证的优点，所以，上下文精化关系很适合用来验证操作系统。但是，现有的支持上下文精化验证方法的工作，大部分都只允许用户程序和对象程序之间有值的传递，而不允许有指针和指针指向的资源的传递。所以，大部分现有的工作都不能支持验证操作系统内核中常见的内存动态分配模块（如常见的malloc和free函数）.在本文中,我们将需要通过指针传递资源的对象称为所有权转移对象。
2、目的（Objective）
我们的目标是将上下文精化关系扩充为可以支持所有权转移对象。具体的目标有：1)为所有权转移对象定义出不暴露实现细节，且能精确描述指针所指向资源的有效性的抽象规范。2)设计一个程序逻辑，用于验证所有权转移对象的实现和抽象规范之间的上下文精化关系。
3、方法（Method）
为了实现目标，我们需要解决以下两个问题：1）怎么在精确描述指针所指向资源的有效性的同时，不暴露出实现相关的细节？2）需要被传递的资源不仅会被用户程序和对象程序共享，在传递之前还会被并发的用户线程共享。怎样在程序逻辑中同时支持这两种共享方式？
对于第一个问题，我们引入全局的抽象状态记录被传递的资源的信息。对于第二个问题，引入全局的抽象状态已经能支持用户程序和对象程序之间的共享，但不支持在并发的用户线程之间共享。所以，我们引入抽象谓词（abstract predicate）的机制，使用一种特殊的抽象资源(称之为代币,token)和可分割的权限机制(fractional permission)来控制信息的分享方式，使用户线程之间可以灵活的分享信息，且不会持有过期的信息。
4、结果（Result&Findings）
首先，我们提出了一种新的方法，能为所有权转移对象定义出不暴露实现细节，且能精确描述所转移资源的有效性的抽象规范。其次，我们设计了一个程序逻辑，用于验证所有权转移对象和抽象规范之间的上下文精化关系，并证明了这个程序逻辑的可靠性。最后，我们成功使用程序逻辑验证了一个现实使用中的操作系统内核的动态内存分配模块（经过适当得到简化）。
5、结论（Conclusions）
我们提供了一种新的可以为所有权转移对象定义抽象规范的方法，并设计了相应的程序逻辑用于验证所有权转移对象的实现和抽象规范之间的上下文精化关系。使用这个程序逻辑，我们成功验证了一个来自于实际使用中的抢占式操作系统内核的动态内存分配模块（经过适当的简化）。
不过，当前工作仍有需要在为工作中去完善的地方。在接下来的工作中，我们需要设计用于验证用户程序调用抽象规范的功能正确性的程序逻辑，从而和现在的工作一起，组成可以验证完整程序功能正确性的框架。