Model Extraction And Model Checking Research For Java Concurrent Programs

With the development of multicore proccessors, concurrent distributed systems become the mainstream of software architectures. The characteristics of distributed software makes the errors nonrecurring, which leads the test and debug process to be extremely hard.Java is the most popular high-level language that supports concurrent in the language level. It has lots of class libraries which can support concurrent programming. Improper use of these class libraries will cause many bugs which are difficult to find but may heavily damage your software. In the same time, Java Memory Model (JMM) allows compilers to change the executing order of programs in the optimization progress. This will lead to lots of unexpected errors in multithreaded Java programs. In Java specification, the correctness of programs just depends on programmers writing right code, which is hard to satisfy high reliable software's requirements.To solve these problems, this paper introduces a set of approach to detect and fix the bugs of multithreaded Java programs. This first part introduces an automated software model checking technique. Based on this, we implemented a tool named JTS that can verify and model checking concurrent Java programs. This technique analyzes Java source code, build abstract syntax tree, and generate abstract program models. In the progress of analyzing, JTS takes special care to model class libraries of Java virtual machine's concurrent mechanism. This tool can accurately simulate the executing path of concurrent Java programs and model checking them with help of SPIN model checker.JTS extracted models from several concurrent Java programs and model checking them successfully with counter examples in the experiment. The models build by JTS accurately reproduced the execution paths of Java programs, which can be used to detect concurrent related hidden bugs. This kind of technique introduced a new direction and method to find and fix bugs that are hard to reproduce, hard to test. JTS is a useful try and complement for traditional testing techniques in the concurrent programming field.This paper brings another new approach which aimed potential order change in Java programs, together with dependences, volatile variables and synchronized code blocks to extract models, and model checking them.To this approach, we show the out of order program models and model checking results. In these simulation executions and model checking counter-paths, we can see how these multithreaded concurrent Java programs executed out of order clearly. This method checks all the execution order changes in codes under nowadays Java specification memory model. So it can find errors which are ignored by other techniques including traditional software model checking, and shows the counter path. This makes a great effort to the proccess of high reliable Java program's verification.