Research On Safety Property Verification For Infinite-State Systems

With the development of VLSI technology,especially the end of Dennard scaling,single core can not meet the needs of hardware development,multi-core has become the mainstream architecture.Multi-thread makes efficient use of hardware resources,but introduces new challenge for parallel programming.The combination of multi-core and multi-thread,and the demand for cross-platform applications need to use the concurrent model to improve the development efficiency of hardware and software.The common concurrency models,such as Petri nets,broadcast protocols,and thread transiton systems are infinite-state systems.Due to the special and diversity for concurrency,the kind of this systems are suffered from state explosion problem for safety verification.The computational and memory overhead is very large,and it is hard to verify this kind of systems efficiently.Well-structured transition systems(WSTS)are a very broad class of infinitestate system,encompassing common models of concurrent systems such as Petri nets,broadcast protocols,thread transition systems,and lossy channel systems.The safety verification problem of WSTS is decidable by coverability analysis.In this paper,we focus on the safety verification problem of WSTS.We propose several safety verification algorithms for this kinds of infinite-state systems by using model checking techniques.First,we focus on the parameterized verification by using Petri nets.Then,we study the general algorithms for WSTS coverability problem.Finally,the proposed algorithms are used to check the safety of multithreaded programs.The significant contributions of this paper are as follows:(1).We present a Petri nets based algorithm for safety verification of parameterized systems.The parameterized system consists of a set of identical,concurrently running components,where the number of components is called system parameters.Due to the infinity number of components,the parameterized system is an infinite-state system.The parameterized verification problem is undecidable.We propose a Petri nets based algorithm for parameterized systems to improve the scalability of safety verification.First,the parameterized system is translated into Petri net by counter abstraction.Then,We use the SAT-based model checker to verify the safety property incrementally.By the combination of counter abstraction and model checking,the scalability of safety property verification is improved.The experimental results show that our algorithm can greatly scale the verification capabilities compared favorably against several recently published approaches.The verification scale of the parameterized protocol is 6?8 times with TDA.(2).We present a fixed point calculation acceleration algorithm for safety verification of WSTS.To solve the safety verification problem of WSTS,we present a fixed point calculation acceleration algorithm.This algorithm is based on the exact backward reachability by using BDDs,and use the IC3 algorithm to compute the over-approximation of backward reachability for accelerating the computation of the fixed point.The experimental results show that by using the IC3 algorithm to accelerate the backward search,we improve the speed of problem solving,especially for the coverable(unsafe)instances.For some instances,the computational speed is more than 100 times with the classical backward search algorithm,and the memory consumption is significantly reduced.(3).We propose a backward over-approximation based algorithm for safety verification WSTS.Due to the high cost in WSTS coverability analysis,we prosed an algorithm for infinite-state system coverability problem by using finite-state model checking algorithms.Firstly,the WSTS is divided into a series of finite-state machines with different weights.Then,the state-of-the-art model checking algorithm is used to compute the over-approximation of the reachability for the finite state machines,incrementally.Finally,the algorithm produces a coverable counterexample path or proves the system is uncoverable.The results show that the algorithm can solve more instances under the same time limit.97.2% instances are solved within 1 GB memory,which is more than two times of the compared algorithms.(4).We propose safety verification algorithm and frame for multithreaded programs.We focus on the safety verification of Pthread-stytle multithreaded programs by using predicate abstraction and model checking techniques.The results show that the new algorithm outperforms the recently published works,especially on memory consumption.We introduce a verification platform for multithreaded programs by integrating many verification tools.All tools work together to solve the problems efficiently.The combination of multiple tools is efficient,and can be used to solve more larger practical problems.