软件精化技术是软件形式方法的基石之一,是保证软件可靠性的重要手段。精化技术可分为逐步精化和精化验证。逐步精化用于递增式开发,通过逐步引入细节来降低开发复杂度以及保证引入细节前后的一致性。精化验证用于实现的正确性验证,许多程序验证问题都可以归结为精化验证。从上世纪七十年代起,人们已对精化技术开展了大量研究。然而在智能体系统、软件事务内存以及弱内存存储模型中,精化关系变得更加复杂,使得验证更加困难。现有的研究工作尚有许多问题亟待解决。本文在对多智能体系统的逐步精化、软件事务内存和写全序弱内存模型的精化验证方面进行了研究,主要工作和创新点如下。1、对情景化多智能体系统的逐步精化进行研究。由于情景化多智能体系统本身具有的复杂性,人们从宏观、中间及微观三个不同的层次来进行开发,为了保证层次之间及层次内的一致性,开发过程中采用形式的递增式开发方法是必要的。在中间层次上,当引入新的智能体时,我们采用Object-Z表示法对系统进行规格说明描述,并且给出基于Object-Z表示法和活动系统迹语义的精化证明责任。宏观层次到中间层次的转换,从用时间段谓词描述的宏观层次规格说明出发,给出带有时间段谓词的规格说明的精化方法,逐步从宏观层次精化为中间层次。2、对软件事务内存实现正确性的精化验证进行了研究。首先简述了事务内存规格说明1准则(Transactional Memory Specification 1,TMS1)及软件事务内存实现TL2-RCAD。针对交换性和引入简单预言变量的前向模拟这两种验证方法不能验证TL2-RCAD正确性的问题,提出了语义交换的验证方法,给出了证明责任,使得一类这两种方法不能验证的软件事务内存实现得到验证。3、给出写全序弱内存模型新操作语义、编译优化和局部程序转换规则的正确性验证。在写全序弱内存模型上,分析了现有操作语义和公理语义的不足,给出了新公理语义以及在此基础上定义的新操作语义,证明了新公理语义和原公理语义的等价性,以及新操作语义与新公理语义的等价性。在新操作语义的基础上,验证了写全序弱内存模型上的编译优化以及局部程序转换规则的正确性。4、针对目前提出的写全序弱内存模型上线性化定义的不足,定义了一个仅使用调用返回接口的新线性化概念,并且证明该线性化与上下文精化之间的等价性,给出了弱内存模型上原子性的规格说明。5、为模块化的验证写全序弱内存模型上线性化,提出基于依赖保证的模拟,给出该模拟保证精化关系的正确性证明。分析了写全序弱内存模型上的循环锁、票循环锁、读-拷贝-更新实现,给出原子性的规格说明,并验证具体实现与规格说明之间的线性化关系。