Research On Concurrent System Modeling And Model Checking Based On Process Algebra

For developing concurrent distributed system, process algebra based model checking is widely considered as a feasible and important approach to reducing errors and increasing system reliability. 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, much research has been done about process algebra based model checking. Main contributions in this thesis are:1. The method called ABSR for verifying safety and liveness property isproposed, which advocates proving properties of a system by checking properties of its components and performs assume-guarantee reasoning in an incremental and fully automated fashion. ABSR can reduce state-space of the system during the compositional verification.2. Partial-order reduction method for process algebra is proposed, by which more redundant states can be reduced. In addition the safety property verification using partial-order reduction is presented, compared with traditional verifying method this one can resume those reduced states.3. A supported tool VerTool (Verifying Tool) is implemented to verify concurrent system using ABSR and partial-order reduction. A-B protocol and Dining Philosophers problem are deeply studied as real cases, efficiency of verification is significantly improved and the complexity is decreased.As the experiment result showing, ABSR only reduces redundant states during compositional verification. Partial-order reduction can do more extensively reduction, In addition the reduced states can be resumed and participated in higher-level model checking. Partial-order reduction availably copes with thestate-explosion problem which does harm to model checking technology.