The Research For Verification Of MSVL Programs Based On Coq

With the rapid development of the Internet and the diversification of software engineering,the complexity and demand of software increase sharply.However,the quality and safety problems of software are increasingly prominent.In recent years,fatal accidents caused by software errors frequently happen.For example,a bug in the floating-point calculation unit of Intel’s Pentium microprocessor chip has made a loss of 475 million dollars in 1994.Therefore,the reliability and security of software are very important and have been paid more and more attention to at large.The traditional way to ensure the quality and safety of software is mainly through software testing,the correctness,reliability and security of system behavior must rely on uninterrupted testing over a long period of time,then gradually find all kinds of problems and correct them in time.But testing is only to prove that there is an error in software and can’t guarantee that there is no error,thus we can see that there is no essential guarantee by testing.So formal method based on strict mathematics is undoubtedly a precise and reliable software technology,it is suitable for the description,development and verification of software and hardware systems especially,and has been highly favored by researchers in mathematics,computer,artificial intelligence,etc.MSVL is a temporal logic programming language for modeling,simulation and verification.As a language with a rich type system,it is a useful formalism for specification and verification of concurrent and real time systems.However,the verification tools for MSVL programs are most based on model checking.Coq is a theorem proving assistant developed by INRIA,it can not only be used to develop security programs,but also proofs from which reliable programs and modules are generated.In this paper,we mainly study a verification method of MSVL programs based on theorem prover Coq,specific research are outlined as follows:(1)Since theorem proving of MSVL programs are not yet well supported by tools,we propose a theorem proving method for MSVL programs based on axiomatic semantics and develop a theorem prover for MSVL programs based on Coq.To this end,first,we describe the variables,expressions and functions of MSVL with the Coq specification language Gallina;then we define MSVL statements and derive statements with Gallina;finally the axiomatic system of MSVL is formalized in Coq.Based on the above definition,MSVL programs can be identified very well in Coq.(2)According to the proposed verification method,for the verification of specific examples,we model the problem with MSVL and extract relevant properties,then use Coq tactics to prove properties in a semi-automatization manner.The proving process performs interactively and adopts backward reasoning,that is,if the preconditions of tactics chosen by user are satisfied,then the current goal will be reduced to one or more subgoals by the application of tactics,some details are automatically proved by Coq,otherwise tactics fail.When all the goals are resolved,the proof is finished,the verification of properties is completed.