The State Space Reduction Based On Partial Order Technology And Its Application In Concurrent System

Along with the growing of the functional requirements of the software and hardware of the system, this leads to the scale of the system more and more complex, the safety and reliability is more and more difficult to be guaranteed. In some key areas, for example,aerospace, bank, bond etc., software reliability is particularly important witch has become one of the major issues in the study. In the past thirty years, Aimed at the uncertainty of concurrent execution systems, researchers in various countries have done a lot of work to solve the reliability problem. model checking is one of the hot spot in this field.Model checking is a formal automated technique that can offer solutions to many of the problems related to software defects. generally speaking, given a formal mathematical model of the system and some formal property, using model checking one can establish if the model satisfies the property. The test results of the the automated checker either confirms that the system satisfies the conditions, or provides a counter-example path. However,for many types of systems, the number of possible states during system execution grows exponentially with the size of the system and the number of the processes, this is the so-called state explosion problem.Partial order reduction is a technique that emphasize this problem for concurrent asynchronous systems by constructing a smaller state space. Indeed, the only requirement is that the modified concurrent composition computes enough interleavings to make checking the desired property possible, not all concurrent executions need be represented if the verification does not require it.In this thesis,we will make a further research on model checking technology and partial order reduction. The main work is as follows:First, detail the Formal description of the concurrent systems and The basic principles ofmodel checking, And study how to use the TLA+ language to specify the real problem.Second, introduce the related theory of partial order reduction, further more, study several partial order algorithm of the state space reduction, like ample sets、persistent sets and conditional stubborn sets.Third, based on the conditional stubborn and persistent computing algorithms. Through the set theory, and under the same condition, we proved that the conditional stubborn sets can more profitably than the persistent sets.Fourth, combining stubborn set and technology of the symmetry reduction, we present a kind of model based on Petri-net, and analysis the reader/writer Mutual exclusion of reduction process. Through the tool LoLA compare the validation.Finally, research the effect evaluation of partial order reduction experiment, we also present the modeling based on Promela language of leader election algorithm, and use SPIN for partial order reduction.