Research On Safety Property Verification For InfiniteState Systems  Posted on:20181230  Degree:Doctor  Type:Dissertation  Country:China  Candidate:L Zhang  Full Text:PDF  GTID:1368330623950407  Subject:Electronic Science and Technology  Abstract/Summary:  PDF Full Text Request  With the development of VLSI technology,especially the end of Dennard scaling,single core can not meet the needs of hardware development,multicore has become the mainstream architecture.Multithread makes efficient use of hardware resources,but introduces new challenge for parallel programming.The combination of multicore and multithread,and the demand for crossplatform 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 infinitestate 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.Wellstructured 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 infinitestate 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 infinitestate 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 SATbased 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 overapproximation 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 overapproximation based algorithm for safety verification WSTS.Due to the high cost in WSTS coverability analysis,we prosed an algorithm for infinitestate system coverability problem by using finitestate model checking algorithms.Firstly,the WSTS is divided into a series of finitestate machines with different weights.Then,the stateoftheart model checking algorithm is used to compute the overapproximation 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 Pthreadstytle 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.  Keywords/Search Tags:  InfiniteState Systems, Safety Property Verification, WellStructured Transition Systems, Petri Net, Multithreaded Program, Formal Verification, Model Checking, IC3  PDF Full Text Request  Related items 
 
