| As the development of the computer system, the study for the advance in the quality of the software is attached more and more importance by the professional. And the key factors for the high qualities of the software systems are the correctness and reliability.Recently, the method which is used frequently in the software verification is testing the large system. By imputing many testing cases and examining the results, we may find the bugs of the system. But by this method, we couldn't perform all the behaviors of the system. At present, model checking has matured into an effective technique for reasoning about realistic components of the hardware systems and the communication protocols, and the applying of the model checking in the software system verification is becoming one of the focuses now. A lot of software model checking tools are already developed by many research groups, such as SLAM,MAGIC,JPF etc.The state explosion problem is the major hurdle in applying model checking to software systems. In this paper, we research two methods for reducing the state-space in the modeling of the Java program model checking, which are the program-slicing and abstract. Our work is in the frame of modeling-verify-refine modeling and based on the open source project JPF (Java PathFinder). The main work in this paper is as follow:1. Introduced the software model checking in the frame of modeling-verify-refine modeling. 2. Based on the formal study of the CFCL(Concurrent Flowchart Language), we researched the bisimulation method for correctness of the multi-thread program slicing .3. Put forward the multi-thread program slicing method. The model checking method combined with the formal modeling language can impulse the automatic software verification observably.4. To handle the spurious counter example which are caused by the program abstract technique, we put forward two methods for finding the feasible counter example in the model checking, which are free-choice search and guided simulation. |
PDF Full Text Request