Research On Coarse Grained Automatic Modeling Method Of Java Multithreaded Programs Oriented To Model Checking

There are many concurrencies,synchronization,and interaction behaviors in the Java multithreaded program,which leads to the explosion of the states,and it is more difficult to detect the algorithm errors in a program.Debugging methods and testing methods are difficult to cover all execution paths in concurrent programs;software model checking methods search all execution paths in concurrent programs automatically,but it is difficult to complete when the state explodes.This thesis proposes a Hierarchical Coloured Petri Net(HCPN)coarse-grained automatic modeling method for Java multithreaded programs,reduce the size of the model and its state space without affecting the results of model checking,which is beneficial to the improvement of model checking efficiency.The work is as follows:1.The processing strategy for property formula is proposed.The coarse-grained model must retain the state information that needs to be detected contained in property formula,and the statement in source program which relates to the state information that needs to be detected must be described in fine-grained.Therefore,this thesis proposes the property formula processing strategies that include the annotation method of related variables,the recognition method of detection-related statements,and the prompt method of the related model fragment.2.A program pre-processing method that contained the judgment method of coarse and fine granularity for statement is proposed.Reading the source program in statement units;constructing the statement binary tree for each function,and judgingand labeling the granularity of the statement in source program according to the judgment strategy of coarse and fine granularity proposed in this thesis.3.Propose the fine-grained and coarse-grained description methods.Functions in the source program are mapped to the model sub-pages,and statements are mapped to different model fragments according to the type of statements.For the specific statements such as concurrency,synchronization,interaction,detection-related statements,etc.,described in fine-grained that map a statement to a model fragment;for other statements,described in coarse-grained that map multiple statements to a model fragment.Using the complex arc expressions to achieve the functional equivalence of a single model fragment and multiple statements.4.The complex arc expression generation method is proposed.HCPN arc expressions use Meta Language(ML)grammar rules,this thesis generates the complex arc expressions in coarse-grained model fragments by superimposing pre-defined templates.In particular,the nesting relationship between the statements in the source program is mapped to the function calls,and the loop structure that not support by ML is mapped to the call of the recursive function.Finally,through the comparative analysis of examples,proved that the coarse-fine-grained modeling method can effectively reduce the size of the model and its state space without affecting the model checking results.