Full Regular Temporal Property Verification as Dynamic Program Execution
Meng Wang, Cong Tian, Zhenhua Duan · 2017
Verification of programs in code-level has attracted more and more attentions since the cost is high to extract models from source code. Most of the approaches available for code-level verification are carried on by inserting assertions into programs and then checking whether the assertions are violated. But in this way, only safety properties can be verified, other temporal properties of programs such as liveness cannot be verified. To tackle this problem, a unified model checking approach is presented in this paper where a program to be verified is written in a Modeling, Simulation and Verification Language (MSVL) program M and a desired property is specified by a Propositional Projection Temporal Logic (PPTL) formula P. Different from the traditional model checking approach, the negation of the desired property is translated into an MSVL program M' first. Then whether P is valid on M can be checked by evaluating whether there exists an acceptable execution of the new MSVL program "M and M'". This problem can be efficiently conducted with the compiler of MSVL namely MSV. The proposed approach has been implemented in a tool called UMC4MSVL. Experiments show that UMC4MSVL is efficient in verifying temporal properties of real-world programs.