MSVL Based Static-Dynamic Program Verification And Automated Planning

Temporal logic,as a specification language,has been utilized to the verification of computer programs,digital circuit,and communication protocol as well as the temporal reasoning in Artificial Intelligence(AI).In addition,temporal logic can be used as a programming language to write programs.A program in a temporal logic programming language is called a temporal logic program,which is actually a temporal logic formula.Different from the traditional imperative programs,such as Pascal and C programs,the execution of a temporal logic program is reducing the formula according to the given rules.It is usually more complicated to execute temporal logic programs and execution efficiency has become a key factor in applying temporal logic programs to practice.To this end,we do a research on compiling and running of programs in Modeling,Simulation and Verification Language(MSVL)and develop a compiler for it.Further,based on MSVL compiler,the verification of C programs and automated planning with MSVL and MSVL compiler are studied.Further,to support the verification of temporal properties of C programs,we do a research on automated mining of full regular temporal properties from C programs.The main contributions are summarized as follows.First,to execute MSVL programs efficiently,an approach to compiling and executing MSVL programs is presented and a compiler for MSVL is developed,including lexical and syntax analysis,preprocessing,semantic analysis,intermediate code generation,and the implementation of runtime system.Among them,we focus on the preprocessing of temporal operators and the implementation of the runtime system for concurrent statements.The compiler takes a well formed MSVL program as input and outputs an executable binary code.Experiments show that the efficiency of MSVL compiler is much higher than that of the existing MSVL interpreter.In addition,simulation,modeling and verification of MSVL programs are implemented based on MSVL compiler.The implementation of MSVL compiler provides a basis for other works,such as the efficient runtime verification of MSVL programs and the unified-dynamic verification of MSVL programs,and in turn these works provide a basis for the verification of C programs in this paper.Second,we present an approach based on MSVL to verifying temporal properties of C programs by means of combining both static analysis and dynamic verification.The desired properties are specified with PPTL formulae.Therefore,some properties that cannot be verified by the existing tools can be dealt with.In addition,abstraction technique is used in the stage of static analysis,which can relieve the state space explosion problem to some extent.Last but not least,on the one hand,because a static analysis is used to find candidate counterexamples,no false negative is produced.On the other hand,a dynamic approach is utilized to check spurious counterexamples,no false positive is produced.The approach has been implemented in a tool named SDMC.Experiments show that SDMC cannot only be used to verify interval related and periodically repeated properties but also outperforms the relevant tools available in verification of simple safety and liveness properties.In addition,SDMC can be used to verify the real world programs.Third,property acquiring is a major problem in the field of program verification.To support the verification of C programs,a dynamic property mining approach is proposed to automatically mine temporal properties from C programs.Different from the existing approaches,it uses PPTL as the property specification language,thus more complex properties such as interval related and periodically repeated properties can be mined.In addition,since invariant detecting tool Daikon is used to detect invariants from the target program,the proposed approach can be used to mine data-temporal properties.Further,since the proposed approach mines temporal properties from the execution traces of the target program and is independent from the source code,it can be used to mine temporal properties from programs in other languages,such as JAVA and C++.Theoretically,the approach can be used to mine temporal properties in PPTL of arbitrary length and complexity.To improve the efficiency of mining,a distributed approach is proposed to mine properties in a parallel way.Fourth,we apply MSVL in the field of automated planning and present a planning approach on the basis of MSVL programs.In this approach,MSVL programs are used to model the planning problem and specify the Search Control Knowledge(SCK)simultaneously.As a result,the planning result can be obtained via executing the MSVL program.To model a planning problem with an MSVL program,an automatic approach is implemented to translate the standard planning domain description language PDDL(Planning Domain Description Language)to MSVL program.We select some typical benchmark problems from the International Planning Competition and experiment with them.The experiments show that the proposed approach is suitable to solve the problems involving temporal information,and our planner is more effective than most of the state-of-the-art planners in some complex planning domains.