软件逐步精化及并发程序精化验证

发布时间：2018-03-10 16:20

本文选题：软件逐步精化　切入点：精化验证　出处：《上海大学》2016年博士论文　论文类型：学位论文

【摘要】：软件精化技术是软件形式方法的基石之一,是保证软件可靠性的重要手段。精化技术可分为逐步精化和精化验证。逐步精化用于递增式开发,通过逐步引入细节来降低开发复杂度以及保证引入细节前后的一致性。精化验证用于实现的正确性验证,许多程序验证问题都可以归结为精化验证。从上世纪七十年代起,人们已对精化技术开展了大量研究。然而在智能体系统、软件事务内存以及弱内存存储模型中,精化关系变得更加复杂,使得验证更加困难。现有的研究工作尚有许多问题亟待解决。本文在对多智能体系统的逐步精化、软件事务内存和写全序弱内存模型的精化验证方面进行了研究,主要工作和创新点如下。1、对情景化多智能体系统的逐步精化进行研究。由于情景化多智能体系统本身具有的复杂性,人们从宏观、中间及微观三个不同的层次来进行开发,为了保证层次之间及层次内的一致性,开发过程中采用形式的递增式开发方法是必要的。在中间层次上,当引入新的智能体时,我们采用Object-Z表示法对系统进行规格说明描述,并且给出基于Object-Z表示法和活动系统迹语义的精化证明责任。宏观层次到中间层次的转换,从用时间段谓词描述的宏观层次规格说明出发,给出带有时间段谓词的规格说明的精化方法,逐步从宏观层次精化为中间层次。2、对软件事务内存实现正确性的精化验证进行了研究。首先简述了事务内存规格说明1准则(Transactional Memory Specification 1,TMS1)及软件事务内存实现TL2-RCAD。针对交换性和引入简单预言变量的前向模拟这两种验证方法不能验证TL2-RCAD正确性的问题,提出了语义交换的验证方法,给出了证明责任,使得一类这两种方法不能验证的软件事务内存实现得到验证。3、给出写全序弱内存模型新操作语义、编译优化和局部程序转换规则的正确性验证。在写全序弱内存模型上,分析了现有操作语义和公理语义的不足,给出了新公理语义以及在此基础上定义的新操作语义,证明了新公理语义和原公理语义的等价性,以及新操作语义与新公理语义的等价性。在新操作语义的基础上,验证了写全序弱内存模型上的编译优化以及局部程序转换规则的正确性。4、针对目前提出的写全序弱内存模型上线性化定义的不足,定义了一个仅使用调用返回接口的新线性化概念,并且证明该线性化与上下文精化之间的等价性,给出了弱内存模型上原子性的规格说明。5、为模块化的验证写全序弱内存模型上线性化,提出基于依赖保证的模拟,给出该模拟保证精化关系的正确性证明。分析了写全序弱内存模型上的循环锁、票循环锁、读-拷贝-更新实现,给出原子性的规格说明,并验证具体实现与规格说明之间的线性化关系。
[Abstract]:Software refinement is one of the cornerstones of software formal methods and an important means to ensure the reliability of software. By gradually introducing details to reduce development complexity and ensure consistency before and after the introduction of details. Refined verification is used to verify the correctness of the implementation, many program verification problems can be attributed to refined verification. A lot of research has been done on the refinement technology. However, in the agent system, software transaction memory and weak memory storage model, the elaboration relationship becomes more complex. It makes verification more difficult. There are still many problems to be solved. In this paper, we study the refinement of multi-agent system, the refinement verification of software transaction memory and write full order weak memory model. The main work and innovations are as follows: 1. The gradual refinement of situational multi-agent system is studied. Because of the complexity of situational multi-agent system, people develop it from three different levels: macro, middle and micro. In order to ensure the consistency between and within the levels, it is necessary to adopt the formal incremental development method in the development process. At the middle level, when introducing new agents, we use Object-Z representation to describe the system specifications. The responsibility of proof based on Object-Z representation and the semantics of active system trace is given. The transformation from macro level to middle level is based on the specification of macro level described by time period predicate. A refined method for specification with time period predicates is given. In this paper, the verification of the correctness of software transaction memory implementation is studied from macro level refinement to intermediate level. Firstly, the transaction memory specification (1) criterion and the software transaction memory implementation (TL2-RCAD) are briefly introduced in this paper, which include the Transactional Memory memory specification 1 (1) and the software transaction memory implementation (TL2-RCAD). The two verification methods, commutativity and forward simulation with simple predictive variables, cannot verify the correctness of TL2-RCAD. In this paper, a verification method of semantic exchange is proposed, and the burden of proof is given, which verifies a class of software transaction memory implementations that cannot be verified by these two methods. The new operation semantics of write full order weak memory model are given. In this paper, the shortcomings of the existing operation semantics and axiom semantics are analyzed, and the new axiom semantics and the new operation semantics defined on this basis are given. The equivalence between the new axiom semantics and the primitive axiom semantics, and the equivalence between the new operation semantics and the new axiom semantics are proved. The correctness of compiling optimization and local program conversion rules on write full order weak memory model is verified. 4. Aiming at the deficiency of linearization definition on write full order weak memory model, A new linearization concept using only the calling return interface is defined, and the equivalence between this linearization and contextual refinement is proved. In this paper, the specification of atomicity on weak memory model is given. 5. Linearization of full order weak memory model for modularized verification is presented, and the simulation based on dependency guarantee is proposed. The correctness of the simulation to ensure the elaboration relationship is proved. The cyclic lock, ticket cyclic lock, read copy update implementation on the write order weak memory model are analyzed, and the atomic specification is given. The linearization relationship between specification and specification is verified.
【学位授予单位】：上海大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：TP311.1

【相似文献】