A Hierarchical CPN Model Automatically Generating Method Aiming at Multithreading Program Algorithm Error Detection

摘要

Due to the uncertainty of concurrency, the detection of algorithm error of multithreading concurrent software is very difficult, and it is difficult to guarantee the correctness. This paper proposes an automatic model generation method, which automatically reads the multithreading JAVA program and generates the Hierarchical Coloured Petri Nets (HCPN) model consistent with the program behavior. Firstly, reading and analyzing the program source program, storing function declarations in the function list, storing global variables in the global variable list, and building a local variable list and a statement binary tree for each function. Secondly, the multithreading program is converted to a HCPN model. Variables in the program correspond to the token-flowing supported by the variable group in the model. The function calls correspond to substitution transitions in the model. Global variables exist in the whole model, and the local variables exist in the function, the subpage model correspond to the function. The preorder traversal statement binary tree obtains the nested or sequential relationships between the statements, converting the program statement into model fragments and then connecting into a complete HCPN model according to the relationship between the statements. Finally, generating a model file conforming to the CPN Tools file format. So that ASK-CTL model checking method in CPN Tools could be used on the generated model for demand attributes, which detecting algorithm errors. Models generated by this method are consistent with source programs, so model errors in model checking are also program errors. Experimental results verify the validity and correctness of the proposed method.