Research On Efficient Runtime Verification For MSVL Programs

Modeling,Simulation and Verification Language(MSVL)is a temporal logic programming language.It is an executable subset of Projection Temporal Logic(PTL).With rich data structures,function calls,and synchronous and asynchronous communication mechanisms,MSVL has been successfully applied to model representation,path simulation and formal verification of concurrent systems,reactive systems and embedded real-time systems.As a propositional subset of PTL,Propositional PTL(PPTL)has full regular expressiveness,which can easily specify sequential,parallel,interval related and periodically repeated prop-erties.Based on the unified PTL logic framework,a runtime verification approach for an MSVL program has been implemented to monitor whether one dynamic execution under scrutiny satisfies a desired PPTL property.However,this verification method still has some short-comings.First,the verification of a temporal property for one single execution path does not make full use of widely existing multi-core devices and distributed networks,which leads to the verification being inefficient.Second,there is no tracking for the dynamically allocat-ed memory areas in the program execution,which makes that memory leaks in a program cannot be timely found.Third,in the verification of a temporal property for a program with several randomly selected branches,it cannot be guaranteed that the discovered counterex-ample is the shortest one,leading to more state spaces being explored.To overcome the above problems,this paper focuses on efficient runtime verification for an MSVL program.The main work is summarized as follows:First of all,we propose a multi-core system based parallel runtime verification approach for an MSVL program.In this approach,the state sequence produced by the program exe-cution is divided into several segments which are verified in parallel.For each segment,a thread pool is created,in which multiple threads are employed to complete the verification.Whenever a certain number of segments have been verified,the verification results for these segments are timely merged to check whether the final result can be obtained.Based on the LLVM platform,we have developed a runtime verifier,namely PPTLCheck.The ex-perimental results show that compared with other verification tools,PPTLCheck has higher verification efficiency and can verify full regular properties for large-scale programs.As a verification case,we also study the verification problem whether several threads can execute alternately as expected in a multi-threaded program.To achieve this,we model the problem in MSVL and specify the desired property by a PPTL formula.After that,PPTLCheck is invoked to verify the dynamic execution of the MSVL program.Secondly,a distributed network based parallel runtime verification approach for an MSVL program is presented.This approach utilizes various kinds of machines in a distributed net-work to concurrently verify segments of a state sequence.In each multi-core machine,a segment can be further divided into several subsegments which are also verified in parallel.To complete the verification task efficiently,we propose a socket communication mechanism to transmit messages between different machines and a scheduling mechanism to distribute verification tasks for different segments.Moreover,an adaptive algorithm is presented to au-tomatically adjust the number of verification threads in each machine.Based on an existing local area network,we have developed a tool called PPTLCheck~+to implement the above method.Experimental results show that PPTLCheck~+is more efficient than PPTLCheck.To check whether the invoking of APIs supplied by SQLite3 conforms to given specifications,we have developed a tool called SQLite3Check.SQLite3Check first analyzes the API speci-fications published on the SQLite3 official website.After these specifications are formalized by corresponding PPTL formulas,PPTLCheck~+is employed to detect API conformance vi-olations for programs invoking APIs of SQLite3.Thirdly,we propose a runtime detection approach for memory leaks of an MSVL program.This approach adopts the dynamic symbolic execution so as to expose memory leaks oc-curring in as many execution paths as possible.During the program execution,a back-end leak checker tracks each dynamically allocated memory area which is accessed.Moreover,it calculates the number of pointers to each memory area so as to detect memory leaks.Besides,the leak location and changes of variables pointing to each memory area are also recorded.After the program execution,corresponding deallocation statements are generated in suitable locations of the source code.Based on KLEE and the MSVL compiler,we have implemented our approach in a tool called DEF LEAK.Experiments show that DEF LEAK can detect more leaks than other dynamic detection tools and is more effective for helping programmers understand and fix memory leaks.Finally,we propose a unified bounded runtime verification approach for MSVL programs with randomly selected branches.Based on the unified runtime verification approach for MSVL and bounded semantics for PPTL,our approach constructs a Bounded Labeled Nor-mal Form Graph(BLNFG)with increasing depth to find the shortest prefix of all paths violating the desired property.This method can be used to show that there is no coun-terexample within a certain search depth in case that the computing resource is limited or there is no need for each whole path to satisfy the property.We conduct the verification for three classical problems including the mutual exclusion problem,dining philosophers problem and banker's algorithm so as to illustrate the feasibility of the presented approach for practical problems.