A CUDA-based Parallel Model Checking Method For Pushdown Systems

Model checking is an important formal verification technique that uses state-space searching to explore all possible system states.In this way,it is possible to check whether a given system satisfies some certain properties.In recent years,model checking has been rapidly developed and has been widely used in many high-security fields,e.g.,aerospace field,rail transit field,automotive electronic field,industrial control field and other fields.Pushdown system is an important model in model checking because of its special mechanism.Model checking on pushdown systems has been widely used in many practical problems,such as program analysis and malware detection.How-ever,there are also two major problems that limit the development of model checking.Firstly,with the complexity of the program,one of the real challenges encountered in model checking is the well-known state explosion problem.Secondly,the efficiency of existing model checking algorithms is always subject to the size of the state space.It is difficult to perform model checking more effectively with limited processor and memo-ries.By now,many techniques are proposed to solve the above problems,e.g.,symbolic model checking approaches,partial-order reduction,symmetry reduction and other tech-nologies.Besides these typical techniques,parallel computing,especially GPUs,has re-cently shown unique advantages in large-scale computing tasks,which has attracted widespread attention from model checking researchers.Some existing model checking researches have achieved good results.Based on the automata theory,this work proposes a general parallel solution for the model-checking problems of pushdown systems,and utilizes the multi-threading of CUDA to accelerate model checking on pushdown systems,e.g.,the reachability analysis and LTL model checking.The main contributions of this thesis are as follows:1.We propose two new models:multi-threaded P-automaton and multi-threaded Buchi pushdown systems.After analyzing the process of model checking algorithms,we propose two multi-threading models that are the extension of the original models These multithreaded models provide a new idea for representing P-automaton and the Biichi pushdown system in the multithreaded parallel framework.2.Base on the traditional algorithms,we design parallel model checking algorithms for pushdown systems.The parallel algorithms distribute compute-intensive tasks over many threads,which provides a new solution for parallel model checking on pushdown systems.In addition,the parallel algorithms are general which can be implemented on a variety of multi-threaded parallel architectures3.Based on CUDA,we design and implement a parallel model checker for pushdown systems.This tool runs on popular GPUs.In order to achieve good speed-up,we design a minimal bit-cost encoding and dynamic task management for itExperimental results show that our parallel method can solve the model check-ing problem of pushdown systems more effectively than the existing model checking method.The performance speed-up achieve up to 100X.