An Approach of Concurrent Object-Oriented Program Slicing Based on LTL Property

Program slicing is a technique for analyzing program by focusing on the statements which have dependence relations with slicing criterion. Slicing has applications in testing and debugging, re-engineering, program comprehension and software maintenance. Program verification is an important method in assuring the correctness and reliability of computer hardware and software. One of the major problems is space-explosion in the application of this method to concurrent software systems: state space grows exponentially in the number of concurrent components. In fact, it is often the case that some of the statements of the program are irrelevant to the verified property and can be deleted. In this paper, we introduce an approach for slicing concurrent object-oriented programs to reduce state space in the process of program verification. Firstly, we define the dependencies between statements in the given program. Then present the method of extracting slicing criterion from linear temporal logic property and propose the steps of computing slicing. We also discussed that the satisfaction of the verified LTL property is guaranteed for both programs before and after slicing, and at the same time the number of states in state transition graph is decreased.