Verifying Full Regular Temporal Properties Of Programs Via Dynamic Program Execution

In order to verify safety,reliability and security properties of software systems in large s-cale,many researchers focus on formal verification.With the traditional model checking,an abstract model has to be extracted from the source code.However,as software systems become larger and more complex,it is difficult to acquire a model consistent with the o-riginal program.In recent years,verifying software systems at code level has become an important research topic.The related research mainly includes three directions as follows:?1?With the reachability analysis approach,error labels are required to be instrumented in a program and then the verification is carried out by checking the reachability of the labels.Only safety properties can be verified in this way,however,verification of other temporal properties such as liveness is not supported.?2?Model checking temporal properties without executing code considers all possible behaviors,which makes small programs generate large state-space.As a result,it is difficult to verify programs in large scale with the approach.Further,sometimes false positives may be produced due to the lack of execution details.?3?Runtime verification checks whether a certain execution path of a system to be verified sat-isfies a given property by monitoring the run of the system.It alleviates the state-explosion problem since only a single execution path is checked each time.Although some research work has been carried out to verify programs at code level,the techniques are far from being mature.Existing tools are incapable of verifying programs in large scale.In this thesis,we focus on formal verification of programs at code level,and the main contributions are summarized as follows:1.For verifying programs in large scale,we propose a formal verification approach to ver-ifying full regular temporal properties of programs via dynamic program execution.With this approach,a program to be verified is written in a Modeling,Simulation and Verification Language as a program₈)and a desired property is specified by a Propositional Projec-tion Temporal Logic?PPTL?formula.Further,?is translated to an MSVL program^?₈).Thus,whether₈)satisfyingis valid can be verified by checking whether there is an acceptable execution path of the new MSVL program“₈)and^?₈)”.Armed with MSVL compiler,“₈)and^?₈)”is compiled to binary code?69??9^?.0?0).The latter is then ex-ecuted with verification cases generated via dynamic symbolic execution.In addition,we employ a parallel mechanism to verify various execution paths of a program for improving the efficiency.The proposed approach has been implemented in a tool called UMC4M and integrated in toolkit MSV.Moreover,to evaluate effectiveness and scalability of MSV,exper-iments including 23 tiny programs,6 programs in medium scale and 10 real world programs whose sizes range from 1.1k to 81k lines have been conducted.The results show that the performance of MSV outperforms existing tools such as T2,RiTHM and LTLAutomizer in temporal properties verification of real-world programs.2.In order to verify desired properties of C programs using UMC4M,we propose a trans-lation approach from a C program to an MSVL program.We confine the syntax of C in a suitable subset called Xd-C in which error-prone and redundant statements are removed from C without loss of expressiveness.MSVL features all Xd-C data types and statements.Therefore,an Xd-C program can be translated to an equivalent MSVL program in a one-to-one manner.We present algorithms to translate declarations,expressions and statements from Xd-C to MSVL.Moreover,we define the equivalence relationship between states,ex-pressions and statements in Xd-C and MSVL.Further,based on the operational semantics of Xd-C and MSVL,we prove equivalences between expressions and statements in Xd-C and MSVL by means of structural induction and rule induction,respectively.Furthermore,we prove the equivalence between an original Xd-C program and the translated MSVL pro-gram.In addition,the proposed approach has been implemented by a tool called C2M.Experiments including 13 real-world Xd-C programs are conducted.The results show that C2M works effectively.3.We apply the runtime verification approach via dynamic program execution to verifica-tion of software systems including a virtual memory management system and a scheduling protocol of a safety-critical system.As a case study,a virtual memory management sys-tem is first modeled by an MSVL program,and then safety and reliability properties of the system are verified.For doing so,we model the Memory Management Unit,Page Fault Handler and External Pager using MSVL programs.Further,some desired properties are formalized and checked.For instance,kernel space cannot be accessed by user processes,and if user space is accessed by user processes,a virtual address can always be transformed to a physical address.Moreover,we apply the verification approach to a scheduling proto-col of a safety-critical system.With the approach,the clock,task,interrupt and scheduler modules are modeled by MSVL programs.Thus,according to the logic relationship among these modules,an MSVL program describing the system can be written.Furthermore,we verify some properties with the theorem proving and runtime verification at code level.For example,the system is schedulable;there is always one and only one executing task if no interrupt occurs;and the task with the highest priority among the requested tasks should first be scheduled.