Automatic Generation Method Of Hierarchical Colored Petri Net Model For Multithreaded JAVA Program

With the wide application of software systems,multithreaded software has become a mainstream software system,and algorithm error detection is becoming more and more important.Due to the uncertainty of the concurrent behavior,the algorithm error detection of the multithreaded JAVA program is very difficult,and the correctness is difficult to guarantee.The traditional model-based detection method has two drawbacks.Firstly,manual modeling,the correctness of the model is difficult to guarantee.Secondly,the modeling workload is large and the efficiency is low.Therefore,this thesis proposes an automatic generation method of Hierarchical Colored Petri Net(HCPN)model for multithreaded JAVA program.On the one hand,the process of generating HCPN model realizes automation and improves modeling efficiency;on the other hand,this thesis aims at modeling the program to ensure the consistency of the program and model.This thesis has done the following work:(1)The method of reading and storing multithreaded program: Reading,analyzing and storing the multithreaded JAVA program.The class declaration,the function declaration,and the variable declaration statement are stored in linked lists.The program processing statements in each function are stored in a statement binary tree,and the nested relationship and the order relationship of the subsequent statements are distinguished by the left and right child nodes of the current statement node in the tree.(2)The method of ganareting HCPN model: The HCPN model is generated based on the program information in the declaration linked list and the statement binary tree.In the model,the token is used to describe the variables in the program,the color set is used to implement the variable type description,and the variable group is used to support the token flow.The object is processed by the tuple according to the data members of the class.Function definitions and function calls are described by model subpages and substitution transitions,multithread concurrency in the program is described by concurrency structure in the model,and the interaction between global variables and static variables in threads is realized by fusion sets.Different types of program processing statements are described by corresponding standard model fragments.The order and nested relationship of program statements are implemented by the connection and nesting of model fragments.(3)The method of generating model file: The generated HCPN model is generated by the CPN Tools standard format file,which can be opened in CPN Tools and model checking by ASK-CTL.Finally,the correctness of the method is verified by the example application and the analysis of execution effect.It shows that the proposed method can automatically generate the HCPN model consistent with the multithreaded JAVA program,and provide the basis of research for the subsequent coarse-grained automatic modeling method and model checking method.