Software Stepwise Refinement And Refinement Verification Of Concurrent Programs

Refinement is one of the cornerstones of formal methods and it is an important means to guarantee software reliability.Refinement can be divided into stepwise refinement and refinement verification.Setpwise refinement is used to incremental development.It reduces the complexity of development by introducing the design decisions step by step,and guarantees the consistency before and after the introduction of details.Refinement verification is to verify the correctness of an implementation.Many program verifications can be reduced to refinement verification.Since 70 s of last century,people have carried out a great deal of work on refinement.However,in the multi-agent system,software transactional memory,and weak memory models,refinement relations become more complex,more difficult to be verified.There are still many problems to be solved in the present research work.This dissertation makes several contributions on stepwise refinement in multi-agent system and refinement verification in software transactional memory and Total Store Order(TSO)-a kind of weak memory model.1.Stepwise refinement is applied to incremental developing suited multi-agent system.Due to inherent complexity of suited multi-agent system,the disciplined engineering of multi-agent system should proceed at three distinct levels of abstraction,macro,meso and micro.To guarantee the correctness between levels and in one level,formal methods and incremental development are necessary.At the meso level,when a new agent is introduced,the system is specified with the notation of Object-Z,and trace semantics is taken for developing proof obligations for refinement.The proof obligations are given in the style of schemes of Object-Z.From the macro to the meso level,the specification at the macro level which is specified by the interval predicates is refined by decreasing the granularity of interval to be the specification at the meso level.2.Refinement verification in software transaction memory(STM).TMS1(Transactional Memory Specification 1)correctness criterion and STM implementation TL2-RCAD are introduced first.To solve the problem that TL2-RCAD cannot be verified by existed two kinks of refinement verification techniques,the commutativity and forward simulation with simple prophecy variable,semantic commutativity and its proof obligations are proposed.Semantic commutativity provides a method for verifying the STM that cannot be verified by the existed two kinds of verification techniques.3.New operational semantics,the refinement verification of compilation and local program transformation rules on TSO are presented.Weakness of existed operational and axiomatic semantics of the TSO weak memory model is analyzed,a new operational semantics is proposed,and the rules of compilation optimization and local program transformation on TSO are verified.4.On account of the weakness of existed linearizability definition in TSO,a new definition of linearizability is proposed,which uses only call and return interfaces of method,this new definition of linearizability is shown to be equivalent to the contextual refinement on TSO,and two kinds of common specifications for the atomicity are given.5.The rely guarantee based simulation is developed for verifying the linearizability on TSO,and its correctness are given.The implementations of spinlock,ticket spinlock and read-copy-update are analyzed,their specifications with atomicity are given,and the linearizability between the implementation and specification is verified.