Research On Model Checking Of Concurrent System Based On Partial-order Reduction

Along with the widespread application of concurrent software system in the essential domains such as the national economy, the national defense and so on, the problem of how to qualify concurrent system's accuracy and the reliability becomes a pressing task. Speaking of the concurrent system, its intrinsic uncertainty makes the problem more difficult than ever. With the analysis of the concurrent system by using formal method, it can search the loophole or the flaws in the system design, and so can help the designers revise and then optimize the system, finally makes the system to be more normative, more effective and more reasonable. In other words, the formal method plays the quite vital role in the entire process of software system development.Model checking is one of the most successful automatic verification techniques in the past two decades. Because of its high level automation and high efficiency, model checking has been widely used in the analysis and verification of concurrent system. However practical application of model checking to real systems has been stymied by the state explosion problem, an exponential growth in the number of states to be explored as the number of processes which composed the system increases.After investigating and analyzing the cause of state explosion problem and the model checking technology tailed for concurrent system, much research has been done. The main contributions in this thesis are in the following:Firstly, CCS, short for Calculus of Communication System, as one of the most famous process algebras used in formal method, is studied. Because of its succinct concept and rich supporting tools available, it has been obtained the widespread application in all aspects of building concurrent system, such as criterion, analysis, design, confirmation and so on. So the CCS as the formal description method is used in this paper to study the concurrent system model. Secondly, the causes of state explosion problem and partial-order reduction technology tailed for concurrent systems are studied. Partial-order reduction method based on process algebra is proposed, by which more redundant states can be reduced and the efficiency of verification can be effectively enhanced.Thirdly, the verification algorithms of safety property and deadlock using partial-order reduction technology are proposed. And these algorithms have been proven validity.At last, a supported tool MCTool (Model Checking Tool) is implemented to verify concurrent system. The five kinds of combination model for concurrent processes have been analyzed. And the typical concurrency models have been test on MCTool for experiment, and the results show that while guaranteeing the correctness of verification results, partial-order reduction technique enhances the verification efficiency in deed.